Theorem 3imtr3d 282

Description: More general version of 3imtr3i 280. 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 229	. 2 |- ( ph -> ( ps -> ta ) )
5	1, 4	sylbird 250	1 |- ( ph -> ( th -> ta ) )

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

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This theorem depends on definitions:  df-bi 197

This theorem is referenced by:  tz6.12i  6214  f1imass  6521  fornex  7135  tposfn2  7374  eroveu  7842  sdomel  8107  ackbij1lem16  9057  ltapr  9867  rpnnen1lem5  11818  rpnnen1lem5OLD  11824  qbtwnre  12030  om2uzlt2i  12750  m1dvdsndvds  15503  pcpremul  15548  pcaddlem  15592  pockthlem  15609  prmreclem6  15625  catidd  16341  ghmf1  17689  gexdvds  17999  sylow1lem1  18013  lt6abl  18296  ablfacrplem  18464  drnginvrn0  18765  issrngd  18861  islssd  18936  znrrg  19914  isphld  19999  cnllycmp  22755  nmhmcn  22920  minveclem7  23206  ioorcl2  23340  itg2seq  23509  dvlip2  23758  mdegmullem  23838  plyco0  23948  pilem3  24207  sincosq1sgn  24250  sincosq2sgn  24251  logcj  24352  argimgt0  24358  lgseisenlem2  25101  eengtrkg  25865  eengtrkge  25866  ubthlem2  27727  minvecolem7  27739  nmcexi  28885  lnconi  28892  pjnormssi  29027  tan2h  33401  itg2gt0cn  33465  divrngcl  33756  lshpcmp  34275  cdlemk35s  36225  cdlemk39s  36227  cdlemk42  36229  dihlspsnat  36622  clcnvlem  37930