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  6690  f1imass  7016  fornex  7651  tposfn2  7908  eroveu  8386  sdomel  8658  ackbij1lem16  9651  ltapr  10461  rpnnen1lem5  12374  qbtwnre  12586  om2uzlt2i  13313  m1dvdsndvds  16129  pcpremul  16174  pcaddlem  16218  pockthlem  16235  prmreclem6  16251  catidd  16945  ghmf1  18381  gexdvds  18703  sylow1lem1  18717  lt6abl  19009  ablfacrplem  19181  drnginvrn0  19514  issrngd  19626  islssd  19701  znrrg  20706  isphld  20792  cnllycmp  23554  nmhmcn  23718  minveclem7  24032  ioorcl2  24167  itg2seq  24337  dvlip2  24586  mdegmullem  24666  plyco0  24776  sincosq1sgn  25078  sincosq2sgn  25079  logcj  25183  argimgt0  25189  lgseisenlem2  25946  eengtrkg  26766  eengtrkge  26767  ubthlem2  28642  minvecolem7  28654  nmcexi  29797  lnconi  29804  pjnormssi  29939  opsbc2ie  30233  qusvscpbl  30915  tan2h  34878  lindsadd  34879  itg2gt0cn  34941  divrngcl  35229  lshpcmp  36118  cdlemk35s  38067  cdlemk39s  38069  cdlemk42  38071  dihlspsnat  38463  clcnvlem  39976  tz6.12i-afv2  43436  sqrtnegnre  43501