MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  3imtr3i Structured version   Visualization version   GIF version

Theorem 3imtr3i 282
Description: A mixed syllogism inference, useful for removing a definition from both sides of an implication. (Contributed by NM, 10-Aug-1994.)
Hypotheses
Ref Expression
3imtr3.1 (𝜑𝜓)
3imtr3.2 (𝜑𝜒)
3imtr3.3 (𝜓𝜃)
Assertion
Ref Expression
3imtr3i (𝜒𝜃)

Proof of Theorem 3imtr3i
StepHypRef Expression
1 3imtr3.2 . . 3 (𝜑𝜒)
2 3imtr3.1 . . 3 (𝜑𝜓)
31, 2sylbir 226 . 2 (𝜒𝜓)
4 3imtr3.3 . 2 (𝜓𝜃)
53, 4sylib 209 1 (𝜒𝜃)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 197
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8
This theorem depends on definitions:  df-bi 198
This theorem is referenced by:  rb-ax1  1832  speimfwALT  2057  cbv1  2440  hblem  2915  axrep1  4965  tfinds2  7293  smores  7685  idssen  8237  1sdom  8402  itunitc1  9527  dominf  9552  dominfac  9680  ssxr  10392  nnwos  11974  pmatcollpw3lem  20801  ppttop  21025  ptclsg  21632  sincosq3sgn  24467  adjbdln  29270  fmptdF  29783  funcnv4mpt  29797  disjdsct  29807  esumpcvgval  30465  esumcvg  30473  measiuns  30605  ballotlemodife  30884  bnj605  31300  bnj594  31305  imagesset  32381  meran1  32727  meran3  32729  bj-modal4e  33020  bj-cbv1v  33043  bj-axrep1  33102  f1omptsnlem  33500  mptsnunlem  33502  topdifinffinlem  33511  relowlpssretop  33528  poimirlem25  33747  eqelb  34323  symrefref3  34623  dedths  34741  mzpincl  37799  lerabdioph  37871  ltrabdioph  37874  nerabdioph  37875  dvdsrabdioph  37876  frege91  38748  frege97  38754  frege98  38755  frege109  38766  sumnnodd  40342  aiotaval  41677
  Copyright terms: Public domain W3C validator