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  5753  fornex  6094  tposfn2  6245  eroveu  6604  ismkvnex  7131  indpi  7304  axcaucvglemres  7861  qsqeqor  10586  caucvgrelemcau  10944  m1dvdsndvds  12202  pcpremul  12247  pcaddlem  12292  pockthlem  12308  limccnpcntop  13438  sincosq1sgn  13541  sincosq2sgn  13542  subctctexmid  14034