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  1626  19.8w  1659  ax10lem2  1877  sbal  2066  hblem  2387  axrep1  4132  tfinds2  4654  smores  6369  idssen  6906  1sdom  7065  itunitc1  8046  dominf  8071  dominfac  8195  ssxr  8892  ltadd2i  8950  nnwos  10286  ppttop  16744  ptclsg  17309  sincosq3sgn  19868  adjbdln  22663  ballotlemodife  23056  fmptdF  23221  funcnv4mpt  23237  disjdsct  23369  meran1  24850  meran3  24852  dstr  25171  mzpincl  26812  lerabdioph  26886  ltrabdioph  26889  nerabdioph  26890  dvdsrabdioph  26891  bnj605  28939  bnj594  28944  ax9lem15  29154
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