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  6904  f1imass  7257  focdmex  7954  tposfn2  8247  naddel1  8699  eroveu  8826  sdomel  9138  ackbij1lem16  10248  ltapr  11059  rpnnen1lem5  12997  qbtwnre  13215  om2uzlt2i  13969  m1dvdsndvds  16818  pcpremul  16863  pcaddlem  16908  pockthlem  16925  prmreclem6  16941  catidd  17692  issgrpd  18708  ghmf1  19229  gexdvds  19565  sylow1lem1  19579  lt6abl  19876  ablfacrplem  20048  isdomn4  20676  drnginvrn0  20714  issrngd  20815  islssd  20892  znrrg  21526  isphld  21614  cnllycmp  24906  nmhmcn  25071  minveclem7  25387  ioorcl2  25525  itg2seq  25695  dvlip2  25952  mdegmullem  26035  plyco0  26149  sincosq1sgn  26459  sincosq2sgn  26460  logcj  26567  argimgt0  26573  lgseisenlem2  27339  sleadd1im  27946  sleadd1  27948  sltonold  28214  onnolt  28219  om2noseqlt2  28246  remulscllem2  28404  eengtrkg  28965  eengtrkge  28966  ubthlem2  30852  minvecolem7  30864  nmcexi  32007  lnconi  32014  pjnormssi  32149  opsbc2ie  32457  qusvscpbl  33366  tan2h  37636  lindsadd  37637  itg2gt0cn  37699  divrngcl  37981  lshpcmp  39006  cdlemk35s  40956  cdlemk39s  40958  cdlemk42  40960  dihlspsnat  41352  clcnvlem  43647  tz6.12i-afv2  47272  sqrtnegnre  47336