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 238	. 2 ⊢ (𝜑 → (𝜓 → 𝜏))
5	1, 4	sylbird 260	1 ⊢ (𝜑 → (𝜃 → 𝜏))

Syntax hints:   → wi 4   ↔ wb 205

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 206

This theorem is referenced by:  tz6.12i  6919  f1imass  7266  focdmex  7946  tposfn2  8239  naddel1  8692  eroveu  8812  sdomel  9130  ackbij1lem16  10236  ltapr  11046  rpnnen1lem5  12972  qbtwnre  13185  om2uzlt2i  13923  m1dvdsndvds  16738  pcpremul  16783  pcaddlem  16828  pockthlem  16845  prmreclem6  16861  catidd  17631  issgrpd  18661  ghmf1  19167  gexdvds  19500  sylow1lem1  19514  lt6abl  19811  ablfacrplem  19983  drnginvrn0  20606  issrngd  20700  islssd  20778  isdomn4  21207  znrrg  21431  isphld  21517  cnllycmp  24802  nmhmcn  24967  minveclem7  25283  ioorcl2  25421  itg2seq  25592  dvlip2  25848  mdegmullem  25934  plyco0  26044  sincosq1sgn  26348  sincosq2sgn  26349  logcj  26454  argimgt0  26460  lgseisenlem2  27223  sleadd1im  27818  sleadd1  27820  sltonold  28067  remulscllem2  28110  eengtrkg  28678  eengtrkge  28679  ubthlem2  30558  minvecolem7  30570  nmcexi  31713  lnconi  31720  pjnormssi  31855  opsbc2ie  32150  qusvscpbl  32903  tan2h  36946  lindsadd  36947  itg2gt0cn  37009  divrngcl  37291  lshpcmp  38324  cdlemk35s  40274  cdlemk39s  40276  cdlemk42  40278  dihlspsnat  40670  clcnvlem  42839  tz6.12i-afv2  46412  sqrtnegnre  46476