Theorem nsyli 158

Description: A negated syllogism inference. (Contributed by NM, 3-May-1994.)

Hypotheses

Ref	Expression
nsyli.1	⊢ (𝜑 → (𝜓 → 𝜒))
nsyli.2	⊢ (𝜃 → ¬ 𝜒)

Assertion

Ref	Expression
nsyli	⊢ (𝜑 → (𝜃 → ¬ 𝜓))

Proof of Theorem nsyli

Step	Hyp	Ref	Expression
1		nsyli.2	. 2 ⊢ (𝜃 → ¬ 𝜒)
2		nsyli.1	. . 3 ⊢ (𝜑 → (𝜓 → 𝜒))
3	2	con3d 153	. 2 ⊢ (𝜑 → (¬ 𝜒 → ¬ 𝜓))
4	1, 3	syl5 35	1 ⊢ (𝜑 → (𝜃 → ¬ 𝜓))

This proof depends on syntax axioms:  ¬ wn 3   → wi 4

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

This theorem is used by:  necon3ad  2973  tz7.7  6390  onssneli  6482  tz7.48-2  8435  tz7.49  8438  php  9198  elirrvOLDOLD  9568  setind  9723  zorn2lem3  10497  alephval2  10576  inar1  10779  ltsres  27881  setindregs  35604  dfon2lem6  36319  finminlem  36890  onint1  37021  poimirlem4  38336  ordnexbtwnsuc  44071  gneispace  44937