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:  exim  1625  dvelimf-o  2231  sspwb  4529  ssopab2b  4604  wetrep  4700  imadif  5481  ssoprab2b  6132  suceloni  6413  tfinds2  6463  iiner  7160  fiint  7576  dfac5lem5  8285  axpowndlem3  8752  axpowndlem3OLD  8753  uzind  10720  isprm5  13780  funcres2  14790  fthres2  14824  ipodrsima  15317  subrgdvds  16802  hausflim  19395  dvres2  21228  axlowdimlem14  23023  atabs2i  25628  nn0prpw  28359  heibor1lem  28549  prter2  28868  pm11.71  29492  sbiota1  29530
  Copyright terms: Public domain W3C validator