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  2968  tz7.7  6383  onssneli  6475  tz7.48-2  8434  tz7.49  8437  php  9204  elirrvOLDOLD  9574  setind  9729  zorn2lem3  10503  alephval2  10584  inar1  10787  ltsres  27901  setindregs  35659  dfon2lem6  36368  finminlem  36940  onint1  37071  poimirlem4  38376  ordnexbtwnsuc  44111  gneispace  44977