Theorem 3imtr3g 555

Description: More general version of 3imtr3i 216. 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 348	. . 3 |- ((ph /\ ps) -> ch)
3		3imtr3g.2	. . . 4 |- (ps <-> th)
4	3	anbi2i 483	. . 3 |- ((ph /\ ps) <-> (ph /\ th))
5		3imtr3g.3	. . 3 |- (ch <-> ta)
6	2, 4, 5	3imtr3i 216	. 2 |- ((ph /\ th) -> ta)
7	6	ex 371	1 |- (ph -> (th -> ta))

Syntax hints:   -> wi 3   <-> wb 144   /\ wa 221

This theorem is referenced by:  3imtr4g 556  dvelimfALT 1190  dvelimf 1288  dvelimALT 1392  sspwb 2835  wetrep 2969  suceloni 3170  tfinds2 3216  imadif 3679  fiint 4703  aceq5lem5 4885  axpowndlem3 5105  lt2msqi 6026  uzind 6376  infxpidmlem12 7775  subtop 7858  dscmet 8129  atabs2i 10611  dfcon2 11501  locfincomp 11575  filfinnfr 11646

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 145  df-an 223

Copyright terms: Public domain