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

Theorem 3imtr3i 265
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 213 . 2  |-  ( ch 
->  ps )
4 3imtr3.3 . 2  |-  ( ps  <->  th )
53, 4sylib 196 1  |-  ( ch 
->  th )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    <-> wb 184
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 185
This theorem is referenced by:  rb-ax1  1569  speimfwOLD  1708  cbv1  1986  sbalOLD  2197  hblem  2590  axrep1  4559  tfinds2  6682  smores  7023  idssen  7560  1sdom  7722  itunitc1  8800  dominf  8825  dominfac  8948  ssxr  9654  ltadd2i  9715  nnwos  11149  pmatcollpw3lem  19079  ppttop  19302  ptclsg  19879  sincosq3sgn  22654  adjbdln  26706  fmptdF  27195  funcnv4mpt  27212  disjdsct  27221  esumpcvgval  27752  esumcvg  27760  measiuns  27856  ballotlemodife  28104  imagesset  29208  meran1  29481  meran3  29483  mzpincl  30298  lerabdioph  30370  ltrabdioph  30373  nerabdioph  30374  dvdsrabdioph  30375  bnj605  33062  bnj594  33067  bj-nalnaleximiOLD  33329  bj-cbv1v  33392  bj-axrep1  33473  bj-hblem  33524  dedths  33783
  Copyright terms: Public domain W3C validator