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  6948  f1imass  7301  focdmex  7996  tposfn2  8289  naddel1  8743  eroveu  8870  sdomel  9190  ackbij1lem16  10303  ltapr  11114  rpnnen1lem5  13046  qbtwnre  13261  om2uzlt2i  14002  m1dvdsndvds  16845  pcpremul  16890  pcaddlem  16935  pockthlem  16952  prmreclem6  16968  catidd  17738  issgrpd  18768  ghmf1  19286  gexdvds  19626  sylow1lem1  19640  lt6abl  19937  ablfacrplem  20109  isdomn4  20738  drnginvrn0  20776  issrngd  20878  islssd  20956  znrrg  21607  isphld  21695  cnllycmp  25007  nmhmcn  25172  minveclem7  25488  ioorcl2  25626  itg2seq  25797  dvlip2  26054  mdegmullem  26137  plyco0  26251  sincosq1sgn  26558  sincosq2sgn  26559  logcj  26666  argimgt0  26672  lgseisenlem2  27438  sleadd1im  28038  sleadd1  28040  sltonold  28301  om2noseqlt2  28324  remulscllem2  28451  eengtrkg  29019  eengtrkge  29020  ubthlem2  30903  minvecolem7  30915  nmcexi  32058  lnconi  32065  pjnormssi  32200  opsbc2ie  32504  qusvscpbl  33344  tan2h  37572  lindsadd  37573  itg2gt0cn  37635  divrngcl  37917  lshpcmp  38944  cdlemk35s  40894  cdlemk39s  40896  cdlemk42  40898  dihlspsnat  41290  clcnvlem  43585  tz6.12i-afv2  47158  sqrtnegnre  47222