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

Theorem 3imtr3i 257
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 205 . 2  |-  ( ch 
->  ps )
4 3imtr3.3 . 2  |-  ( ps  <->  th )
53, 4sylib 189 1  |-  ( ch 
->  th )
Colors of variables: wff set class
Syntax hints:    -> wi 4    <-> wb 177
This theorem is referenced by:  rb-ax1  1523  speimfw  1652  19.8wOLD  1700  ax10lem2OLD  1988  sbal  2163  hblem  2493  axrep1  4264  tfinds2  4785  smores  6552  idssen  7090  1sdom  7249  itunitc1  8235  dominf  8260  dominfac  8383  ssxr  9080  ltadd2i  9138  nnwos  10478  ppttop  16996  ptclsg  17570  sincosq3sgn  20277  adjbdln  23436  fmptdF  23913  funcnv4mpt  23928  disjdsct  23933  esumpcvgval  24266  esumcvg  24274  measiuns  24367  ballotlemodife  24536  meran1  25877  meran3  25879  mzpincl  26484  lerabdioph  26558  ltrabdioph  26561  nerabdioph  26562  dvdsrabdioph  26563  bnj605  28618  bnj594  28623  sbalNEW7  28951
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 178
  Copyright terms: Public domain W3C validator