Theorem 3imtr3g 425

Description: More general version of 3imtr3 191. 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 277	. . 3 |- ((ph /\ ps) -> ch)
3		3imtr3g.2	. . . 4 |- (ps <-> th)
4	3	anbi2i 367	. . 3 |- ((ph /\ ps) <-> (ph /\ th))
5		3imtr3g.3	. . 3 |- (ch <-> ta )
6	2, 4, 5	3imtr3 191	. 2 |- ((ph /\ th) -> ta )
7	6	exp 291	1 |- (ph -> (th -> ta ))

Syntax hints:   -> wi 2   <-> wb 127   /\ wa 196

This theorem is referenced by:  3imtr4g 426  ddelimf2 907  ddelimf 908  sspwb 1863  wetrep 2194  suceloni 2314  tfinds2 2405  imadif 2714  fiint 3445  aceq5lem5 3562  axpowndlem3 3745  lt2sq 4414  infxpidmlem12 4944

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

This theorem depends on definitions:  df-bi 128  df-an 198

metamath.org