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  5853  focdmex  6210  tposfn2  6362  eroveu  6723  ismkvnex  7269  indpi  7468  axcaucvglemres  8025  qsqeqor  10808  caucvgrelemcau  11341  m1dvdsndvds  12621  pcpremul  12666  pcaddlem  12712  pockthlem  12729  issgrpd  13294  ghmf1  13659  islssmd  14171  znrrg  14472  limccnpcntop  15197  sincosq1sgn  15348  sincosq2sgn  15349  lgseisenlem2  15598  subctctexmid  16052  neap0mkv  16123