Theorem 3imtr3g 331

Description: More general version of 3imtr3i 327. Useful for converting definitions in a formula. (The proof was shortened by Wolf Lammen, 7-Nov-2012.)

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.1	. 2 |- (ph -> (ps -> ch))
2		3imtr3g.2	. . 3 |- (ps <-> th)
3	2	a1i 8	. 2 |- (ph -> (ps <-> th))
4		3imtr3g.3	. . 3 |- (ch <-> ta)
5	4	a1i 8	. 2 |- (ph -> (ch <-> ta))
6	1, 3, 5	3imtr3d 329	1 |- (ph -> (th -> ta))

Syntax hints:   -> wi 3   <-> wb 219

This theorem is referenced by:  3imtr4g 332  dvelimfALT 1794  dvelimfALT2 1858  dvelimf 1897  dvelimALT 2008  hblemd 2241  sspwb 3667  wetrep 3805  suceloni 4037  tfinds2 4083  imadif 4593  oprabid 5002  fiint 5872  aceq5lem5 6193  axpowndlem3 6469  lt2msqi 7397  uzind 7760  infxpidmlem12OLD 9226  subtop 9767  dscmet 10062  atabs2i 12805  dfcon2 16266  locfincomp 16338  filfinnfr 16385  prter2 17109  pm11.71 17178  dvelimfALT2OLD 17190

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7

This theorem depends on definitions:  df-bi 220

Copyright terms: Public domain