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  5974  focdmex  6338  tposfn2  6531  eroveu  6894  ismkvnex  7489  indpi  7703  axcaucvglemres  8260  qsqeqor  11070  caucvgrelemcau  11729  m1dvdsndvds  13010  pcpremul  13055  pcaddlem  13101  pockthlem  13118  issgrpd  13710  ghmf1  14059  islssmd  14679  znrrg  14978  limccnpcntop  15759  sincosq1sgn  15910  sincosq2sgn  15911  lgseisenlem2  16173  subctctexmid  17013  neap0mkv  17093