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

Theorem 3imtr3g 262
Description: More general version of 3imtr3i 258. 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 211 . 2  |-  ( ph  ->  ( th  ->  ch ) )
4 3imtr3g.3 . 2  |-  ( ch  <->  ta )
53, 4syl6ib 219 1  |-  ( ph  ->  ( th  ->  ta ) )
Colors of variables: wff set class
Syntax hints:    -> wi 4    <-> wb 178
This theorem is referenced by:  exim  1585  dvelimhwOLD  1880  ax12olem2OLD  2016  dvelimhOLD  2076  dvelimALT  2217  dvelimf-o  2264  sspwb  4448  ssopab2b  4516  wetrep  4610  suceloni  4828  tfinds2  4878  imadif  5563  ssoprab2b  6167  iiner  7012  fiint  7419  dfac5lem5  8046  axpowndlem3  8512  uzind  10399  isprm5  13150  funcres2  14133  fthres2  14167  ipodrsima  14629  subrgdvds  15920  hausflim  18051  dvres2  19837  atabs2i  23943  axlowdimlem14  25929  nn0prpw  26368  heibor1lem  26560  prter2  26842  pm11.71  27685  sbiota1  27723  dvelimhwNEW7  29629  ax12olem2wAUX7  29630  dvelimhvAUX7  29666  dvelimALTNEW7  29810  ax7w17lem2AUX7  29850  ax12olem2OLD7  29880  dvelimhOLD7  29887
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 179
  Copyright terms: Public domain W3C validator