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  5843  focdmex  6200  tposfn2  6352  eroveu  6713  ismkvnex  7257  indpi  7455  axcaucvglemres  8012  qsqeqor  10795  caucvgrelemcau  11291  m1dvdsndvds  12571  pcpremul  12616  pcaddlem  12662  pockthlem  12679  issgrpd  13244  ghmf1  13609  islssmd  14121  znrrg  14422  limccnpcntop  15147  sincosq1sgn  15298  sincosq2sgn  15299  lgseisenlem2  15548  subctctexmid  15937  neap0mkv  16008