Theorem 3imtr3d 295

Description: More general version of 3imtr3i 293. 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 241	. 2 ⊢ (𝜑 → (𝜓 → 𝜏))
5	1, 4	sylbird 262	1 ⊢ (𝜑 → (𝜃 → 𝜏))

Syntax hints:   → wi 4   ↔ wb 208

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 209

This theorem is referenced by:  tz6.12i  6696  f1imass  7022  fornex  7657  tposfn2  7914  eroveu  8392  sdomel  8664  ackbij1lem16  9657  ltapr  10467  rpnnen1lem5  12381  qbtwnre  12593  om2uzlt2i  13320  m1dvdsndvds  16135  pcpremul  16180  pcaddlem  16224  pockthlem  16241  prmreclem6  16257  catidd  16951  ghmf1  18387  gexdvds  18709  sylow1lem1  18723  lt6abl  19015  ablfacrplem  19187  drnginvrn0  19520  issrngd  19632  islssd  19707  znrrg  20712  isphld  20798  cnllycmp  23560  nmhmcn  23724  minveclem7  24038  ioorcl2  24173  itg2seq  24343  dvlip2  24592  mdegmullem  24672  plyco0  24782  sincosq1sgn  25084  sincosq2sgn  25085  logcj  25189  argimgt0  25195  lgseisenlem2  25952  eengtrkg  26772  eengtrkge  26773  ubthlem2  28648  minvecolem7  28660  nmcexi  29803  lnconi  29810  pjnormssi  29945  opsbc2ie  30239  qusvscpbl  30920  tan2h  34899  lindsadd  34900  itg2gt0cn  34962  divrngcl  35250  lshpcmp  36139  cdlemk35s  38088  cdlemk39s  38090  cdlemk42  38092  dihlspsnat  38484  clcnvlem  40003  tz6.12i-afv2  43462  sqrtnegnre  43527