ILE Home 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-1 5  ax-2 6  ax-mp 7  ax-ia1 105  ax-ia2 106  ax-ia3 107
This theorem depends on definitions:  df-bi 116
This theorem is referenced by:  dcn  787  dcan  883  xordc1  1336  hbxfrbi  1413  nfalt  1522  19.29r  1564  19.31r  1623  sbimi  1701  spsbbi  1779  sbi2v  1827  euan  2011  2exeu  2047  ralimi2  2446  reximi2  2481  r19.28av  2519  r19.29r  2521  elex  2644  rmoan  2829  rmoimi2  2832  sseq2  3063  rabss2  3119  unssdif  3250  inssdif  3251  unssin  3254  inssun  3255  rabn0r  3328  undif4  3364  ssdif0im  3366  inssdif0im  3369  ssundifim  3385  ralf0  3405  prmg  3583  difprsnss  3597  snsspw  3630  pwprss  3671  pwtpss  3672  uniin  3695  intss  3731  iuniin  3762  iuneq1  3765  iuneq2  3768  iundif2ss  3817  iinuniss  3833  iunpwss  3842  intexrabim  4010  exmidundif  4058  exmidundifim  4059  exss  4078  pwunss  4134  soeq2  4167  ordunisuc2r  4359  peano5  4441  reliin  4589  coeq1  4624  coeq2  4625  cnveq  4641  dmeq  4667  dmin  4675  dmcoss  4734  rncoeq  4738  resiexg  4790  dminss  4879  imainss  4880  dfco2a  4965  euiotaex  5030  fununi  5116  fof  5268  f1ocnv  5301  rexrnmpt  5481  isocnv  5628  isotr  5633  oprabid  5719  dmtpos  6059  tposfn  6076  smores  6095  eqer  6364  ixpeq2  6509  enssdom  6559  fiprc  6612  fiintim  6719  ltexprlemlol  7258  ltexprlemupu  7260  recexgt0  8154  peano2uz2  8952  eluzp1p1  9143  peano2uz  9170  zq  9210  ubmelfzo  9760  frecuzrdgtcl  9968  frecuzrdgfunlem  9975  expclzaplem  10110  hashfiv01gt1  10321  fsum2dlemstep  10992  sin02gt0  11218  qredeu  11521  bj-indint  12538
  Copyright terms: Public domain W3C validator