Theorem 3imtr3g 551

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 552  dvelimfALT 1151  dvelimf 1248  dvelimALT 1351  sspwb 2750  wetrep 2937  suceloni 3057  tfinds2 3160  imadif 3566  fiint 4540  aceq5lem5 4719  axpowndlem3 4931  lt2msq 5837  uzind 6161  infxpidmlem12 7514  subtop 7596  dscmet 7870  atabs2 10266

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