Theorem 3imtr3d 296

Description: More general version of 3imtr3i 294. 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 242	. 2 ⊢ (𝜑 → (𝜓 → 𝜏))
5	1, 4	sylbird 263	1 ⊢ (𝜑 → (𝜃 → 𝜏))

Syntax hints:   → wi 4   ↔ wb 209

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 210

This theorem is referenced by:  tz6.12i  6671  f1imass  7000  fornex  7639  tposfn2  7897  eroveu  8375  sdomel  8648  ackbij1lem16  9646  ltapr  10456  rpnnen1lem5  12368  qbtwnre  12580  om2uzlt2i  13314  m1dvdsndvds  16125  pcpremul  16170  pcaddlem  16214  pockthlem  16231  prmreclem6  16247  catidd  16943  ghmf1  18379  gexdvds  18701  sylow1lem1  18715  lt6abl  19008  ablfacrplem  19180  drnginvrn0  19513  issrngd  19625  islssd  19700  znrrg  20257  isphld  20343  cnllycmp  23561  nmhmcn  23725  minveclem7  24039  ioorcl2  24176  itg2seq  24346  dvlip2  24598  mdegmullem  24679  plyco0  24789  sincosq1sgn  25091  sincosq2sgn  25092  logcj  25197  argimgt0  25203  lgseisenlem2  25960  eengtrkg  26780  eengtrkge  26781  ubthlem2  28654  minvecolem7  28666  nmcexi  29809  lnconi  29816  pjnormssi  29951  opsbc2ie  30246  qusvscpbl  30971  tan2h  35049  lindsadd  35050  itg2gt0cn  35112  divrngcl  35395  lshpcmp  36284  cdlemk35s  38233  cdlemk39s  38235  cdlemk42  38237  dihlspsnat  38629  clcnvlem  40323  tz6.12i-afv2  43799  sqrtnegnre  43864