Theorem 3imtr3d 202

Description: More general version of 3imtr3i 200. Useful for converting conditional definitions in a formula. (Contributed by NM, 8-Apr-1996.)

Hypotheses

Ref	Expression
3imtr3d.1	|- ( ph -> ( ps -> ch ) )
3imtr3d.2	|- ( ph -> ( ps <-> th ) )
3imtr3d.3	|- ( ph -> ( ch <-> ta ) )

Assertion

Ref	Expression
3imtr3d	|- ( ph -> ( th -> ta ) )

Proof of Theorem 3imtr3d

Step	Hyp	Ref	Expression
1		3imtr3d.2	. 2 |- ( ph -> ( ps <-> th ) )
2		3imtr3d.1	. . 3 |- ( ph -> ( ps -> ch ) )
3		3imtr3d.3	. . 3 |- ( ph -> ( ch <-> ta ) )
4	2, 3	sylibd 149	. 2 |- ( ph -> ( ps -> ta ) )
5	1, 4	sylbird 170	1 |- ( ph -> ( th -> ta ) )

Syntax hints:   -> wi 4   <-> wb 105

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108

This theorem depends on definitions:  df-bi 117

This theorem is referenced by:  f1imass  5803  focdmex  6148  tposfn2  6299  eroveu  6660  ismkvnex  7193  indpi  7381  axcaucvglemres  7938  qsqeqor  10677  caucvgrelemcau  11036  m1dvdsndvds  12297  pcpremul  12342  pcaddlem  12388  pockthlem  12405  issgrpd  12905  ghmf1  13245  islssmd  13718  limccnpcntop  14682  sincosq1sgn  14785  sincosq2sgn  14786  lgseisenlem2  14990  subctctexmid  15290  neap0mkv  15358