Theorem 3imtr3g 284

Description: More general version of 3imtr3i 280. 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

Step	Hyp	Ref	Expression
1		3imtr3g.2	. . 3 |- ( ps <-> th )
2		3imtr3g.1	. . 3 |- ( ph -> ( ps -> ch ) )
3	1, 2	syl5bir 233	. 2 |- ( ph -> ( th -> ch ) )
4		3imtr3g.3	. 2 |- ( ch <-> ta )
5	3, 4	syl6ib 241	1 |- ( ph -> ( th -> ta ) )

Syntax hints:   -> wi 4   <-> wb 196

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 197

This theorem is referenced by:  aleximi  1759  sspwb  4917  ssopab2b  5002  wetrep  5107  imadif  5973  ssoprab2b  6712  suceloni  7013  tfinds2  7063  iiner  7819  fiint  8237  dfac5lem5  8950  axpowndlem3  9421  uzind  11469  isprm5  15419  funcres2  16558  fthres2  16592  ipodrsima  17165  subrgdvds  18794  hausflim  21785  dvres2  23676  axlowdimlem14  25835  atabs2i  29261  esum2dlem  30154  nn0prpw  32318  bj-hbext  32701  heibor1lem  33608  prter2  34166  dvelimf-o  34214  frege70  38227  frege72  38229  frege93  38250  frege110  38267  frege120  38277  pm11.71  38597  sbiota1  38635