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

Theorem 3imtr3g 269
Description: More general version of 3imtr3i 265. Useful for converting definitions in a formula. (Contributed by NM, 20-May-1996.) (Proof shortened by Wolf Lammen, 20-Dec-2013.)
Hypotheses
Ref Expression
3imtr3g.1  |-  ( ph  ->  ( ps  ->  ch ) )
3imtr3g.2  |-  ( ps  <->  th )
3imtr3g.3  |-  ( ch  <->  ta )
Assertion
Ref Expression
3imtr3g  |-  ( ph  ->  ( th  ->  ta ) )

Proof of Theorem 3imtr3g
StepHypRef Expression
1 3imtr3g.2 . . 3  |-  ( ps  <->  th )
2 3imtr3g.1 . . 3  |-  ( ph  ->  ( ps  ->  ch ) )
31, 2syl5bir 218 . 2  |-  ( ph  ->  ( th  ->  ch ) )
4 3imtr3g.3 . 2  |-  ( ch  <->  ta )
53, 4syl6ib 226 1  |-  ( ph  ->  ( th  ->  ta ) )
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:  aleximi  1623  eximOLD  1625  dvelimf-o  2238  sspwb  4644  ssopab2b  4718  wetrep  4816  imadif  5596  ssoprab2b  6247  suceloni  6529  tfinds2  6579  iiner  7277  fiint  7694  dfac5lem5  8403  axpowndlem3  8870  axpowndlem3OLD  8871  uzind  10839  isprm5  13911  funcres2  14922  fthres2  14956  ipodrsima  15449  subrgdvds  16997  hausflim  19681  dvres2  21515  axlowdimlem14  23348  atabs2i  25953  nn0prpw  28661  heibor1lem  28851  prter2  29169  pm11.71  29793  sbiota1  29831  bj-hbext  32513
  Copyright terms: Public domain W3C validator