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  5970  focdmex  6334  tposfn2  6527  eroveu  6890  ismkvnex  7485  indpi  7699  axcaucvglemres  8256  qsqeqor  11065  caucvgrelemcau  11724  m1dvdsndvds  13005  pcpremul  13050  pcaddlem  13096  pockthlem  13113  issgrpd  13704  ghmf1  14053  islssmd  14668  znrrg  14967  limccnpcntop  15699  sincosq1sgn  15850  sincosq2sgn  15851  lgseisenlem2  16104  subctctexmid  16944  neap0mkv  17024