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  6848  f1imass  7198  focdmex  7888  tposfn2  8178  naddel1  8602  eroveu  8736  sdomel  9037  ackbij1lem16  10125  ltapr  10936  rpnnen1lem5  12879  qbtwnre  13098  om2uzlt2i  13858  m1dvdsndvds  16710  pcpremul  16755  pcaddlem  16800  pockthlem  16817  prmreclem6  16833  catidd  17586  issgrpd  18638  ghmf1  19159  gexdvds  19497  sylow1lem1  19511  lt6abl  19808  ablfacrplem  19980  isdomn4  20632  drnginvrn0  20670  issrngd  20771  islssd  20869  znrrg  21503  isphld  21592  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  28965  eengtrkge  28966  ubthlem2  30849  minvecolem7  30861  nmcexi  32004  lnconi  32011  pjnormssi  32146  opsbc2ie  32453  qusvscpbl  33314  tan2h  37658  lindsadd  37659  itg2gt0cn  37721  divrngcl  38003  lshpcmp  39033  cdlemk35s  40982  cdlemk39s  40984  cdlemk42  40986  dihlspsnat  41378  clcnvlem  43662  tz6.12i-afv2  47280  sqrtnegnre  47344