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  1562  dvelimhw  1735  ax12olem2  1869  dvelimh  1904  dvelimALT  2072  dvelimf-o  2119  sspwb  4223  ssopab2b  4291  wetrep  4386  suceloni  4604  tfinds2  4654  imadif  5327  ssoprab2b  5905  iiner  6731  fiint  7133  dfac5lem5  7754  axpowndlem3  8221  uzind  10103  isprm5  12791  funcres2  13772  fthres2  13806  ipodrsima  14268  subrgdvds  15559  hausflim  17676  dvres2  19262  atabs2i  22982  axlowdimlem14  24583  nn0prpw  26239  heibor1lem  26533  prter2  26749  pm11.71  27596  sbiota1  27634  dvelimfALT2OLD  29125
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