Theorem 3imtr3g 552

Description: More general version of 3imtr3 218. Useful for converting definitions in a formula.

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	. . . 4 |- (ph -> (ps -> ch))
2	1	imp 350	. . 3 |- ((ph /\ ps) -> ch)
3		3imtr3g.2	. . . 4 |- (ps <-> th)
4	3	anbi2i 480	. . 3 |- ((ph /\ ps) <-> (ph /\ th))
5		3imtr3g.3	. . 3 |- (ch <-> ta)
6	2, 4, 5	3imtr3 218	. 2 |- ((ph /\ th) -> ta)
7	6	ex 373	1 |- (ph -> (th -> ta))

Syntax hints:   -> wi 3   <-> wb 146   /\ wa 223

This theorem is referenced by:  3imtr4g 553  dvelimfALT 1153  dvelimf 1250  dvelimALT 1353  sspwb 2755  wetrep 2942  suceloni 3062  tfinds2 3165  imadif 3574  fiint 4559  fiintOLD 4560  aceq5lem5 4739  axpowndlem3 4951  lt2msq 5881  uzind 6205  infxpidmlem12 7563  subtop 7646  dscmet 7918  atabs2 10329

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 147  df-an 225

Copyright terms: Public domain