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  7283  focdmex  7978  tposfn2  8271  naddel1  8723  eroveu  8850  sdomel  9162  ackbij1lem16  10271  ltapr  11082  rpnnen1lem5  13020  qbtwnre  13237  om2uzlt2i  13988  m1dvdsndvds  16831  pcpremul  16876  pcaddlem  16921  pockthlem  16938  prmreclem6  16954  catidd  17724  issgrpd  18755  ghmf1  19276  gexdvds  19616  sylow1lem1  19630  lt6abl  19927  ablfacrplem  20099  isdomn4  20732  drnginvrn0  20770  issrngd  20872  islssd  20950  znrrg  21601  isphld  21689  cnllycmp  25001  nmhmcn  25166  minveclem7  25482  ioorcl2  25620  itg2seq  25791  dvlip2  26048  mdegmullem  26131  plyco0  26245  sincosq1sgn  26554  sincosq2sgn  26555  logcj  26662  argimgt0  26668  lgseisenlem2  27434  sleadd1im  28034  sleadd1  28036  sltonold  28297  om2noseqlt2  28320  remulscllem2  28447  eengtrkg  29015  eengtrkge  29016  ubthlem2  30899  minvecolem7  30911  nmcexi  32054  lnconi  32061  pjnormssi  32196  opsbc2ie  32503  qusvscpbl  33358  tan2h  37598  lindsadd  37599  itg2gt0cn  37661  divrngcl  37943  lshpcmp  38969  cdlemk35s  40919  cdlemk39s  40921  cdlemk42  40923  dihlspsnat  41315  clcnvlem  43612  tz6.12i-afv2  47192  sqrtnegnre  47256