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  1564  dvelimhw  1737  ax12olem2  1871  dvelimh  1906  dvelimALT  2074  dvelimf-o  2121  sspwb  4225  ssopab2b  4293  wetrep  4388  suceloni  4606  tfinds2  4656  imadif  5329  ssoprab2b  5907  iiner  6733  fiint  7135  dfac5lem5  7756  axpowndlem3  8223  uzind  10105  isprm5  12793  funcres2  13774  fthres2  13808  ipodrsima  14270  subrgdvds  15561  hausflim  17678  dvres2  19264  atabs2i  22984  axlowdimlem14  24585  nn0prpw  26250  heibor1lem  26544  prter2  26760  pm11.71  27607  sbiota1  27645  dvelimfALT2OLD  29198
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