Theorem 3imtr3d 202

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

Syntax hints:   → wi 4   ↔ wb 105

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

This theorem depends on definitions:  df-bi 117

This theorem is referenced by:  f1imass  5904  focdmex  6266  tposfn2  6418  eroveu  6781  ismkvnex  7330  indpi  7537  axcaucvglemres  8094  qsqeqor  10880  caucvgrelemcau  11499  m1dvdsndvds  12779  pcpremul  12824  pcaddlem  12870  pockthlem  12887  issgrpd  13453  ghmf1  13818  islssmd  14331  znrrg  14632  limccnpcntop  15357  sincosq1sgn  15508  sincosq2sgn  15509  lgseisenlem2  15758  subctctexmid  16395  neap0mkv  16467