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  1559  speimfw  1697  cbv1  1961  sbalOLD  2175  hblem  2546  axrep1  4403  tfinds2  6473  smores  6812  idssen  7353  1sdom  7514  itunitc1  8588  dominf  8613  dominfac  8736  ssxr  9443  ltadd2i  9504  nnwos  10921  ppttop  18610  ptclsg  19187  sincosq3sgn  21961  adjbdln  25486  fmptdF  25971  funcnv4mpt  25988  disjdsct  25997  esumpcvgval  26526  esumcvg  26534  measiuns  26630  ballotlemodife  26879  imagesset  27983  meran1  28256  meran3  28258  mzpincl  29068  lerabdioph  29141  ltrabdioph  29144  nerabdioph  29145  dvdsrabdioph  29146  bnj605  31898  bnj594  31903  bj-nalnaleximiOLD  32163  bj-cbv1v  32226  bj-axrep1  32307  bj-hblem  32358  dedths  32611
  Copyright terms: Public domain W3C validator