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  5891  focdmex  6250  tposfn2  6402  eroveu  6763  ismkvnex  7310  indpi  7517  axcaucvglemres  8074  qsqeqor  10859  caucvgrelemcau  11477  m1dvdsndvds  12757  pcpremul  12802  pcaddlem  12848  pockthlem  12865  issgrpd  13431  ghmf1  13796  islssmd  14308  znrrg  14609  limccnpcntop  15334  sincosq1sgn  15485  sincosq2sgn  15486  lgseisenlem2  15735  subctctexmid  16297  neap0mkv  16368