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

Theorem 3imtr3i 268
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 216 . 2  |-  ( ch 
->  ps )
4 3imtr3.3 . 2  |-  ( ps  <->  th )
53, 4sylib 199 1  |-  ( ch 
->  th )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    <-> wb 187
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 188
This theorem is referenced by:  rb-ax1  1631  speimfwOLD  1786  cbv1  2073  hblem  2552  axrep1  4539  tfinds2  6704  smores  7079  idssen  7621  1sdom  7781  itunitc1  8848  dominf  8873  dominfac  8996  ssxr  9702  ltadd2iOLD  9765  nnwos  11226  pmatcollpw3lem  19738  ppttop  19953  ptclsg  20561  sincosq3sgn  23320  adjbdln  27571  fmptdF  28095  funcnv4mpt  28113  disjdsct  28123  esumpcvgval  28738  esumcvg  28746  measiuns  28878  ballotlemodife  29156  bnj605  29506  bnj594  29511  imagesset  30505  meran1  30856  meran3  30858  bj-nalnaleximiOLD  31001  bj-cbv1v  31072  bj-axrep1  31154  bj-hblem  31209  f1omptsnlem  31472  mptsnunlem  31474  topdifinffinlem  31484  relowlpssretop  31501  poimirlem25  31672  dedths  32246  mzpincl  35288  lerabdioph  35360  ltrabdioph  35363  nerabdioph  35364  dvdsrabdioph  35365  frege91  36190  frege97  36196  frege98  36197  frege109  36208  sumnnodd  37285
  Copyright terms: Public domain W3C validator