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

Theorem 3imtr4i 194
Description: A mixed syllogism inference, useful for applying a definition to both sides of an implication. (Contributed by NM, 5-Aug-1993.)
Hypotheses
Ref Expression
3imtr4.1 (𝜑𝜓)
3imtr4.2 (𝜒𝜑)
3imtr4.3 (𝜃𝜓)
Assertion
Ref Expression
3imtr4i (𝜒𝜃)

Proof of Theorem 3imtr4i
StepHypRef Expression
1 3imtr4.2 . . 3 (𝜒𝜑)
2 3imtr4.1 . . 3 (𝜑𝜓)
31, 2sylbi 118 . 2 (𝜒𝜓)
4 3imtr4.3 . 2 (𝜃𝜓)
53, 4sylibr 141 1 (𝜒𝜃)
Colors of variables: wff set class
Syntax hints:  wi 4  wb 102
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 103  ax-ia2 104  ax-ia3 105
This theorem depends on definitions:  df-bi 114
This theorem is referenced by:  dcn  757  dcan  853  xordc1  1300  hbxfrbi  1377  nfalt  1486  19.29r  1528  19.31r  1587  sbimi  1663  spsbbi  1741  sbi2v  1788  euan  1972  2exeu  2008  ralimi2  2398  reximi2  2432  r19.28av  2466  r19.29r  2468  elex  2583  rmoan  2762  rmoimi2  2765  sseq2  2995  rabss2  3051  unssdif  3200  inssdif  3201  unssin  3204  inssun  3205  rabn0r  3272  undif4  3312  ssdif0im  3314  inssdif0im  3319  ssundifim  3334  ralf0  3352  prmg  3517  difprsnss  3530  snsspw  3563  pwprss  3604  pwtpss  3605  uniin  3628  intss  3664  iuniin  3695  iuneq1  3698  iuneq2  3701  iundif2ss  3750  iinuniss  3765  iunpwss  3771  intexrabim  3935  exss  3991  pwunss  4048  soeq2  4081  ordunisuc2r  4268  peano5  4349  reliin  4487  coeq1  4521  coeq2  4522  cnveq  4537  dmeq  4563  dmin  4571  dmcoss  4629  rncoeq  4633  resiexg  4681  dminss  4766  imainss  4767  dfco2a  4849  euiotaex  4911  fununi  4995  fof  5134  f1ocnv  5167  rexrnmpt  5338  isocnv  5479  isotr  5484  oprabid  5565  dmtpos  5902  tposfn  5919  smores  5938  eqer  6169  enssdom  6273  fiprc  6323  ltexprlemlol  6758  ltexprlemupu  6760  recexgt0  7645  peano2uz2  8404  eluzp1p1  8594  peano2uz  8622  zq  8658  elfzmlbmOLD  9091  ubmelfzo  9158  frecuzrdgfn  9362  expclzaplem  9444  bj-indint  10442  peano5setOLD  10452
  Copyright terms: Public domain W3C validator