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

Theorem 3imtr4i 200
 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 120 . 2 (𝜒𝜓)
4 3imtr4.3 . 2 (𝜃𝜓)
53, 4sylibr 133 1 (𝜒𝜃)
 Colors of variables: wff set class Syntax hints:   → wi 4   ↔ wb 104 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107 This theorem depends on definitions:  df-bi 116 This theorem is referenced by:  dcn  827  stdcn  832  dcan  918  xordc1  1371  hbxfrbi  1448  nfalt  1557  19.29r  1600  19.31r  1659  sbimi  1737  spsbbi  1816  sbi2v  1864  euan  2055  2exeu  2091  ralimi2  2492  reximi2  2528  r19.28av  2568  r19.29r  2570  elex  2697  rmoan  2884  rmoimi2  2887  sseq2  3121  rabss2  3180  unssdif  3311  inssdif  3312  unssin  3315  inssun  3316  rabn0r  3389  undif4  3425  ssdif0im  3427  inssdif0im  3430  ssundifim  3446  ralf0  3466  prmg  3644  difprsnss  3658  snsspw  3691  pwprss  3732  pwtpss  3733  uniin  3756  intss  3792  iuniin  3823  iuneq1  3826  iuneq2  3829  iundif2ss  3878  iinuniss  3895  iunpwss  3904  intexrabim  4078  exmidundif  4129  exmidundifim  4130  exss  4149  pwunss  4205  soeq2  4238  ordunisuc2r  4430  peano5  4512  reliin  4661  coeq1  4696  coeq2  4697  cnveq  4713  dmeq  4739  dmin  4747  dmcoss  4808  rncoeq  4812  resiexg  4864  dminss  4953  imainss  4954  dfco2a  5039  euiotaex  5104  fununi  5191  fof  5345  f1ocnv  5380  rexrnmpt  5563  isocnv  5712  isotr  5717  oprabid  5803  dmtpos  6153  tposfn  6170  smores  6189  eqer  6461  ixpeq2  6606  enssdom  6656  fiprc  6709  fiintim  6817  ltexprlemlol  7417  ltexprlemupu  7419  recexgt0  8349  peano2uz2  9165  eluzp1p1  9358  peano2uz  9385  zq  9425  ubmelfzo  9984  frecuzrdgtcl  10192  frecuzrdgfunlem  10199  expclzaplem  10324  hashfiv01gt1  10535  fsum2dlemstep  11210  sin02gt0  11477  qredeu  11785  bj-stim  12984  bj-stan  12985  bj-stal  12987  bj-nfalt  13001  bj-indint  13159
 Copyright terms: Public domain W3C validator