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

Theorem 3imtr3i 256
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  |-  ( ph  ->  ps )
3imtr3.2  |-  ( ph  <->  ch )
3imtr3.3  |-  ( ps  <->  th )
Assertion
Ref Expression
3imtr3i  |-  ( ch 
->  th )

Proof of Theorem 3imtr3i
StepHypRef Expression
1 3imtr3.2 . . 3  |-  ( ph  <->  ch )
2 3imtr3.1 . . 3  |-  ( ph  ->  ps )
31, 2sylbir 204 . 2  |-  ( ch 
->  ps )
4 3imtr3.3 . 2  |-  ( ps  <->  th )
53, 4sylib 188 1  |-  ( ch 
->  th )
Colors of variables: wff set class
Syntax hints:    -> wi 4    <-> wb 176
This theorem is referenced by:  rb-ax1  1507  speimfw  1635  19.8wOLD  1678  ax10lem2  1890  sbal  2079  hblem  2400  axrep1  4148  tfinds2  4670  smores  6385  idssen  6922  1sdom  7081  itunitc1  8062  dominf  8087  dominfac  8211  ssxr  8908  ltadd2i  8966  nnwos  10302  ppttop  16760  ptclsg  17325  sincosq3sgn  19884  adjbdln  22679  ballotlemodife  23072  fmptdF  23236  funcnv4mpt  23252  disjdsct  23384  meran1  24922  meran3  24924  dstr  25274  mzpincl  26915  lerabdioph  26989  ltrabdioph  26992  nerabdioph  26993  dvdsrabdioph  26994  bnj605  29255  bnj594  29260  sbalNEW7  29588  ax9lem15  29776
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8
This theorem depends on definitions:  df-bi 177
  Copyright terms: Public domain W3C validator