MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  3imtr3i Structured version   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  1526  speimfw  1655  19.8wOLD  1705  cbv1  1973  ax10lem2OLD  2026  sbal  2203  hblem  2539  axrep1  4313  tfinds2  4835  smores  6606  idssen  7144  1sdom  7303  itunitc1  8290  dominf  8315  dominfac  8438  ssxr  9135  ltadd2i  9194  nnwos  10534  ppttop  17061  ptclsg  17637  sincosq3sgn  20398  adjbdln  23576  fmptdF  24059  funcnv4mpt  24075  disjdsct  24080  esumpcvgval  24458  esumcvg  24466  measiuns  24561  ballotlemodife  24745  imagesset  25763  meran1  26126  meran3  26128  mzpincl  26745  lerabdioph  26819  ltrabdioph  26822  nerabdioph  26823  dvdsrabdioph  26824  bnj605  29179  bnj594  29184  sbalNEW7  29517  ax7w13AUX7  29574
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