Theorem 3imtr3g 550

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 479	. . 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 551  dvelimfALT 1149  dvelimf 1245  sspwb 2745  wetrep 2932  suceloni 3052  tfinds2 3155  imadif 3560  fiint 4534  aceq5lem5 4711  axpowndlem3 4923  lt2msq 5829  uzind 6153  infxpidmlem12 7506  subtop 7588  dscmet 7856  atabs2 10237

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