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  2972  tz7.7  6395  onssneli  6487  tz7.48-2  8466  tz7.49  8469  php  9236  elirrvOLDOLD  9606  setind  9761  zorn2lem3  10589  alephval2  10670  inar1  10873  ltsres  28034  erscottd  35825  setindregs  35872  j0ltaleph  35965  prconf1acwevd  36005  dfon2lem6  36680  finminlem  37236  onint1  37367  poimirlem4  38685  ordnexbtwnsuc  44412  gneispace  45277