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  1632  eximOLD  1634  dvelimf-o  2252  sspwb  4696  ssopab2b  4774  wetrep  4872  imadif  5661  ssoprab2b  6336  suceloni  6626  tfinds2  6676  iiner  7380  fiint  7793  dfac5lem5  8504  axpowndlem3  8971  axpowndlem3OLD  8972  uzind  10948  isprm5  14105  funcres2  15118  fthres2  15152  ipodrsima  15645  subrgdvds  17223  hausflim  20214  dvres2  22048  axlowdimlem14  23931  atabs2i  26994  nn0prpw  29716  heibor1lem  29906  prter2  30224  pm11.71  30881  sbiota1  30919  bj-hbext  33346
  Copyright terms: Public domain W3C validator