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

Theorem 3imtr3g 260
Description: More general version of 3imtr3i 256. 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 209 . 2  |-  ( ph  ->  ( th  ->  ch ) )
4 3imtr3g.3 . 2  |-  ( ch  <->  ta )
53, 4syl6ib 217 1  |-  ( ph  ->  ( th  ->  ta ) )
Colors of variables: wff set class
Syntax hints:    -> wi 4    <-> wb 176
This theorem is referenced by:  exim  1565  dvelimhw  1747  ax12olem2  1881  dvelimh  1917  dvelimALT  2085  dvelimf-o  2132  sspwb  4239  ssopab2b  4307  wetrep  4402  suceloni  4620  tfinds2  4670  imadif  5343  ssoprab2b  5921  iiner  6747  fiint  7149  dfac5lem5  7770  axpowndlem3  8237  uzind  10119  isprm5  12807  funcres2  13788  fthres2  13822  ipodrsima  14284  subrgdvds  15575  hausflim  17692  dvres2  19278  atabs2i  22998  axlowdimlem14  24655  nn0prpw  26342  heibor1lem  26636  prter2  26852  pm11.71  27699  sbiota1  27737  dvelimhwNEW7  29432  ax12olem2wAUX7  29433  dvelimhvAUX7  29469  ax12olem2OLD7  29660  dvelimhOLD7  29667  dvelimfALT2OLD  29747
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 177
  Copyright terms: Public domain W3C validator