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  5925  focdmex  6286  tposfn2  6475  eroveu  6838  ismkvnex  7397  indpi  7605  axcaucvglemres  8162  qsqeqor  10958  caucvgrelemcau  11603  m1dvdsndvds  12884  pcpremul  12929  pcaddlem  12975  pockthlem  12992  issgrpd  13558  ghmf1  13923  islssmd  14438  znrrg  14739  limccnpcntop  15469  sincosq1sgn  15620  sincosq2sgn  15621  lgseisenlem2  15873  subctctexmid  16705  neap0mkv  16785