MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  3imtr3g 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  1581  dvelimhw  1861  ax12olem2OLD  1966  dvelimh  2003  dvelimALT  2167  dvelimf-o  2214  axi11e  2366  sspwb  4354  ssopab2b  4422  wetrep  4516  suceloni  4733  tfinds2  4783  imadif  5468  ssoprab2b  6070  iiner  6912  fiint  7319  dfac5lem5  7941  axpowndlem3  8407  uzind  10293  isprm5  13039  funcres2  14022  fthres2  14056  ipodrsima  14518  subrgdvds  15809  hausflim  17934  dvres2  19666  atabs2i  23753  axlowdimlem14  25608  nn0prpw  26017  heibor1lem  26209  prter2  26421  pm11.71  27265  sbiota1  27303  dvelimhwNEW7  28793  ax12olem2wAUX7  28794  dvelimhvAUX7  28830  dvelimALTNEW7  28969  ax12olem2OLD7  29022  dvelimhOLD7  29029
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