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	⊢ (𝜑 → (𝜓 → 𝜒))
3imtr3d.2	⊢ (𝜑 → (𝜓 ↔ 𝜃))
3imtr3d.3	⊢ (𝜑 → (𝜒 ↔ 𝜏))

Assertion

Ref	Expression
3imtr3d	⊢ (𝜑 → (𝜃 → 𝜏))

Proof of Theorem 3imtr3d

Step	Hyp	Ref	Expression
1		3imtr3d.2	. 2 ⊢ (𝜑 → (𝜓 ↔ 𝜃))
2		3imtr3d.1	. . 3 ⊢ (𝜑 → (𝜓 → 𝜒))
3		3imtr3d.3	. . 3 ⊢ (𝜑 → (𝜒 ↔ 𝜏))
4	2, 3	sylibd 229	. 2 ⊢ (𝜑 → (𝜓 → 𝜏))
5	1, 4	sylbird 250	1 ⊢ (𝜑 → (𝜃 → 𝜏))

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  6357  f1imass  6667  fornex  7286  tposfn2  7530  eroveu  7999  sdomel  8267  ackbij1lem16  9263  ltapr  10073  rpnnen1lem5  12026  qbtwnre  12235  om2uzlt2i  12958  m1dvdsndvds  15710  pcpremul  15755  pcaddlem  15799  pockthlem  15816  prmreclem6  15832  catidd  16548  ghmf1  17897  gexdvds  18206  sylow1lem1  18220  lt6abl  18503  ablfacrplem  18672  drnginvrn0  18975  issrngd  19071  islssd  19146  znrrg  20129  isphld  20216  cnllycmp  22975  nmhmcn  23139  minveclem7  23425  ioorcl2  23560  itg2seq  23729  dvlip2  23978  mdegmullem  24058  plyco0  24168  pilem3OLD  24428  sincosq1sgn  24471  sincosq2sgn  24472  logcj  24573  argimgt0  24579  lgseisenlem2  25322  eengtrkg  26086  eengtrkge  26087  ubthlem2  28067  minvecolem7  28079  nmcexi  29225  lnconi  29232  pjnormssi  29367  tan2h  33733  itg2gt0cn  33796  divrngcl  34086  lshpcmp  34795  cdlemk35s  36745  cdlemk39s  36747  cdlemk42  36749  dihlspsnat  37141  clcnvlem  38454