Theorem syl2im 38

Description: Replace two antecedents. Implication-only version of syl2an 289. (Contributed by Wolf Lammen, 14-May-2013.)

Hypotheses

Ref	Expression
syl2im.1	⊢ (𝜑 → 𝜓)
syl2im.2	⊢ (𝜒 → 𝜃)
syl2im.3	⊢ (𝜓 → (𝜃 → 𝜏))

Assertion

Ref	Expression
syl2im	⊢ (𝜑 → (𝜒 → 𝜏))

Proof of Theorem syl2im

Step	Hyp	Ref	Expression
1		syl2im.1	. 2 ⊢ (𝜑 → 𝜓)
2		syl2im.2	. . 3 ⊢ (𝜒 → 𝜃)
3		syl2im.3	. . 3 ⊢ (𝜓 → (𝜃 → 𝜏))
4	2, 3	syl5 32	. 2 ⊢ (𝜓 → (𝜒 → 𝜏))
5	1, 4	syl 14	1 ⊢ (𝜑 → (𝜒 → 𝜏))

This proof depends on syntax axioms:   → wi 4

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7

This theorem is used by:  syl2imc  39  sylc  62  bi3ant  224  pm3.12dc  971  pm3.13dc  972  nfrimi  1578  abnex  4593  vtoclr  4823  funopg  5411  xpider  6880  rerecapb  9174  ixxssixx  10306  difelfzle  10543  txcnp  15374  uspgr2wlkeqi  16620  bj-inf2vnlem1  17008