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

Theorem 3imtr3g 269
Description: More general version of 3imtr3i 265. 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 218 . 2  |-  ( ph  ->  ( th  ->  ch ) )
4 3imtr3g.3 . 2  |-  ( ch  <->  ta )
53, 4syl6ib 226 1  |-  ( ph  ->  ( th  ->  ta ) )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    <-> wb 184
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 185
This theorem is referenced by:  aleximi  1674  eximOLD  1676  sspwb  4640  ssopab2b  4717  wetrep  4816  imadif  5644  ssoprab2b  6335  suceloni  6631  tfinds2  6681  iiner  7420  fiint  7831  dfac5lem5  8540  axpowndlem3  9006  uzind  10995  isprm5  14462  funcres2  15511  fthres2  15545  ipodrsima  16119  subrgdvds  17763  hausflim  20774  dvres2  22608  axlowdimlem14  24675  atabs2i  27734  esum2dlem  28539  nn0prpw  30551  bj-hbext  30828  heibor1lem  31587  prter2  31904  dvelimf-o  31952  frege70  35914  frege72  35916  frege93  35937  frege110  35954  frege120  35964  pm11.71  36151  sbiota1  36189
  Copyright terms: Public domain W3C validator