Theorem 3imtr3d 201

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

Syntax hints:   → wi 4   ↔ wb 104

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107

This theorem depends on definitions:  df-bi 116

This theorem is referenced by:  f1imass  5741  fornex  6080  tposfn2  6230  eroveu  6588  ismkvnex  7115  indpi  7279  axcaucvglemres  7836  qsqeqor  10561  caucvgrelemcau  10918  m1dvdsndvds  12176  pcpremul  12221  pcaddlem  12266  pockthlem  12282  limccnpcntop  13244  sincosq1sgn  13347  sincosq2sgn  13348  subctctexmid  13841