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

Theorem 3imtr3i 294
 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 238 . 2 (𝜒𝜓)
4 3imtr3.3 . 2 (𝜓𝜃)
53, 4sylib 221 1 (𝜒𝜃)
 Colors of variables: wff setvar class Syntax hints:   → wi 4   ↔ wb 209 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 210 This theorem is referenced by:  rb-ax1  1754  speimfwALT  1967  cbv1v  2345  cbv1  2411  hblem  2920  hblemg  2921  nfcriiOLD  2949  axrep1  5156  tfinds2  7565  smores  7979  idssen  8544  1sdom  8712  itunitc1  9838  dominf  9863  dominfac  9991  ssxr  10706  nnwos  12310  pmatcollpw3lem  21402  ppttop  21626  ptclsg  22234  sincosq3sgn  25107  adjbdln  29880  fmptdF  30433  funcnv4mpt  30446  disjdsct  30476  esumpcvgval  31483  esumcvg  31491  measiuns  31622  ballotlemodife  31901  bnj605  32325  bnj594  32330  acycgr0v  32544  prclisacycgr  32547  imagesset  33563  meran1  33908  meran3  33910  bj-modal4e  34202  f1omptsnlem  34793  mptsnunlem  34795  topdifinffinlem  34804  relowlpssretop  34821  poimirlem25  35122  eqelb  35702  symrefref3  36000  dedths  36298  sn-axrep5v  39440  dffltz  39679  mzpincl  39739  lerabdioph  39810  ltrabdioph  39813  nerabdioph  39814  dvdsrabdioph  39815  frege91  40719  frege97  40725  frege98  40726  frege109  40737  sumnnodd  42333  aiotaval  43711  rrx2linest  45215
 Copyright terms: Public domain W3C validator