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  6889  f1imass  7242  focdmex  7937  tposfn2  8230  naddel1  8654  eroveu  8788  sdomel  9094  ackbij1lem16  10194  ltapr  11005  rpnnen1lem5  12947  qbtwnre  13166  om2uzlt2i  13923  m1dvdsndvds  16776  pcpremul  16821  pcaddlem  16866  pockthlem  16883  prmreclem6  16899  catidd  17648  issgrpd  18664  ghmf1  19185  gexdvds  19521  sylow1lem1  19535  lt6abl  19832  ablfacrplem  20004  isdomn4  20632  drnginvrn0  20670  issrngd  20771  islssd  20848  znrrg  21482  isphld  21570  cnllycmp  24862  nmhmcn  25027  minveclem7  25342  ioorcl2  25480  itg2seq  25650  dvlip2  25907  mdegmullem  25990  plyco0  26104  sincosq1sgn  26414  sincosq2sgn  26415  logcj  26522  argimgt0  26528  lgseisenlem2  27294  sleadd1im  27901  sleadd1  27903  sltonold  28169  onnolt  28174  om2noseqlt2  28201  remulscllem2  28359  eengtrkg  28920  eengtrkge  28921  ubthlem2  30807  minvecolem7  30819  nmcexi  31962  lnconi  31969  pjnormssi  32104  opsbc2ie  32412  qusvscpbl  33329  tan2h  37613  lindsadd  37614  itg2gt0cn  37676  divrngcl  37958  lshpcmp  38988  cdlemk35s  40938  cdlemk39s  40940  cdlemk42  40942  dihlspsnat  41334  clcnvlem  43619  tz6.12i-afv2  47248  sqrtnegnre  47312