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  5907  focdmex  6269  tposfn2  6423  eroveu  6786  ismkvnex  7338  indpi  7545  axcaucvglemres  8102  qsqeqor  10889  caucvgrelemcau  11512  m1dvdsndvds  12792  pcpremul  12837  pcaddlem  12883  pockthlem  12900  issgrpd  13466  ghmf1  13831  islssmd  14344  znrrg  14645  limccnpcntop  15370  sincosq1sgn  15521  sincosq2sgn  15522  lgseisenlem2  15771  subctctexmid  16479  neap0mkv  16551