Theorem 3imtr3d 293

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

Syntax hints:   → wi 4   ↔ wb 206

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 207

This theorem is referenced by:  tz6.12i  6934  f1imass  7284  focdmex  7980  tposfn2  8273  naddel1  8725  eroveu  8852  sdomel  9164  ackbij1lem16  10274  ltapr  11085  rpnnen1lem5  13023  qbtwnre  13241  om2uzlt2i  13992  m1dvdsndvds  16836  pcpremul  16881  pcaddlem  16926  pockthlem  16943  prmreclem6  16959  catidd  17723  issgrpd  18743  ghmf1  19264  gexdvds  19602  sylow1lem1  19616  lt6abl  19913  ablfacrplem  20085  isdomn4  20716  drnginvrn0  20754  issrngd  20856  islssd  20933  znrrg  21584  isphld  21672  cnllycmp  24988  nmhmcn  25153  minveclem7  25469  ioorcl2  25607  itg2seq  25777  dvlip2  26034  mdegmullem  26117  plyco0  26231  sincosq1sgn  26540  sincosq2sgn  26541  logcj  26648  argimgt0  26654  lgseisenlem2  27420  sleadd1im  28020  sleadd1  28022  sltonold  28283  om2noseqlt2  28306  remulscllem2  28433  eengtrkg  29001  eengtrkge  29002  ubthlem2  30890  minvecolem7  30902  nmcexi  32045  lnconi  32052  pjnormssi  32187  opsbc2ie  32495  qusvscpbl  33379  tan2h  37619  lindsadd  37620  itg2gt0cn  37682  divrngcl  37964  lshpcmp  38989  cdlemk35s  40939  cdlemk39s  40941  cdlemk42  40943  dihlspsnat  41335  clcnvlem  43636  tz6.12i-afv2  47255  sqrtnegnre  47319