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  6854  f1imass  7204  focdmex  7894  tposfn2  8184  naddel1  8608  eroveu  8742  sdomel  9044  ackbij1lem16  10132  ltapr  10943  rpnnen1lem5  12881  qbtwnre  13100  om2uzlt2i  13860  m1dvdsndvds  16712  pcpremul  16757  pcaddlem  16802  pockthlem  16819  prmreclem6  16835  catidd  17588  issgrpd  18640  ghmf1  19160  gexdvds  19498  sylow1lem1  19512  lt6abl  19809  ablfacrplem  19981  isdomn4  20633  drnginvrn0  20671  issrngd  20772  islssd  20870  znrrg  21504  isphld  21593  cnllycmp  24883  nmhmcn  25048  minveclem7  25363  ioorcl2  25501  itg2seq  25671  dvlip2  25928  mdegmullem  26011  plyco0  26125  sincosq1sgn  26435  sincosq2sgn  26436  logcj  26543  argimgt0  26549  lgseisenlem2  27315  sleadd1im  27931  sleadd1  27933  sltonold  28199  onnolt  28204  om2noseqlt2  28231  remulscllem2  28404  eengtrkg  28966  eengtrkge  28967  ubthlem2  30853  minvecolem7  30865  nmcexi  32008  lnconi  32015  pjnormssi  32150  opsbc2ie  32457  qusvscpbl  33323  tan2h  37673  lindsadd  37674  itg2gt0cn  37736  divrngcl  38018  lshpcmp  39108  cdlemk35s  41057  cdlemk39s  41059  cdlemk42  41061  dihlspsnat  41453  clcnvlem  43741  tz6.12i-afv2  47368  sqrtnegnre  47432