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

Theorem 3imtr3g 261
Description: More general version of 3imtr3i 257. 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 210 . 2  |-  ( ph  ->  ( th  ->  ch ) )
4 3imtr3g.3 . 2  |-  ( ch  <->  ta )
53, 4syl6ib 218 1  |-  ( ph  ->  ( th  ->  ta ) )
Colors of variables: wff set class
Syntax hints:    -> wi 4    <-> wb 177
This theorem is referenced by:  exim  1584  dvelimhwOLD  1877  ax12olem2OLD  2012  dvelimhOLD  2068  dvelimALT  2209  dvelimf-o  2256  sspwb  4405  ssopab2b  4473  wetrep  4567  suceloni  4785  tfinds2  4835  imadif  5520  ssoprab2b  6123  iiner  6968  fiint  7375  dfac5lem5  8000  axpowndlem3  8466  uzind  10353  isprm5  13104  funcres2  14087  fthres2  14121  ipodrsima  14583  subrgdvds  15874  hausflim  18005  dvres2  19791  atabs2i  23897  axlowdimlem14  25886  nn0prpw  26307  heibor1lem  26499  prter2  26711  pm11.71  27554  sbiota1  27592  dvelimhwNEW7  29382  ax12olem2wAUX7  29383  dvelimhvAUX7  29419  dvelimALTNEW7  29563  ax7w17lem2AUX7  29603  ax12olem2OLD7  29633  dvelimhOLD7  29640
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