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 ) )

This proof depends on syntax axioms:   -> wi 4   <-> wb 105

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108

This proof depends on definitions:  df-bi 117

This theorem is used by:  f1imass  5983  focdmex  6348  tposfn2  6542  eroveu  6905  ismkvnex  7501  indpi  7715  axcaucvglemres  8272  qsqeqor  11107  caucvgrelemcau  11767  m1dvdsndvds  13055  pcpremul  13100  pcaddlem  13146  pockthlem  13163  issgrpd  13785  ghmf1  14134  islssmd  14804  znrrg  15103  limccnpcntop  15918  sincosq1sgn  16070  sincosq2sgn  16071  lgseisenlem2  16412  subctctexmid  17252  neap0mkv  17343