ILE Home Intuitionistic Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  ILE Home  >  Th. List  >  syl5ibrcom Structured version   GIF version

Theorem syl5ibrcom 146
Description: A mixed syllogism inference. (Contributed by NM, 20-Jun-2007.)
Hypotheses
Ref Expression
syl5ibr.1 (φθ)
syl5ibr.2 (χ → (ψθ))
Assertion
Ref Expression
syl5ibrcom (φ → (χψ))

Proof of Theorem syl5ibrcom
StepHypRef Expression
1 syl5ibr.1 . . 3 (φθ)
2 syl5ibr.2 . . 3 (χ → (ψθ))
31, 2syl5ibr 145 . 2 (χ → (φψ))
43com12 27 1 (φ → (χψ))
Colors of variables: wff set class
Syntax hints:  wi 4  wb 98
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 99  ax-ia2 100  ax-ia3 101
This theorem depends on definitions:  df-bi 110
This theorem is referenced by:  biimprcd  149  elsnc2g  3379  preqr1g  3511  opth1  3947  euotd  3965  reusv3  4142  alxfr  4143  reuhypd  4153  ordsucim  4176  suc11g  4219  nlimsucg  4226  onpsssuc  4231  xpsspw  4377  funcnvuni  4894  fvmptdv2  5185  foco2  5243  fsn  5260  fconst2g  5301  funfvima  5315  isores3  5380  eusvobj2  5422  ovmpt2dv2  5557  ovelrn  5572  f1opw2  5629  suppssfv  5631  suppssov1  5632  nnmordi  6000  nnmord  6001  qsss  6076  eroveu  6108  th3qlem1  6119  addnidpig  6196  enq0tr  6289  prcdnql  6338  prcunqu  6339  genipv  6363  genpelvl  6366  genpelvu  6367  distrlem5prl  6425  distrlem5pru  6426  mulid1  6626  ltne  6701  cnegex  6782  bj-peano4  7324
  Copyright terms: Public domain W3C validator