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  2970  tz7.7  6387  onssneli  6479  tz7.48-2  8434  tz7.49  8437  php  9204  elirrvOLDOLD  9574  setind  9729  zorn2lem3  10503  alephval2  10584  inar1  10787  ltsres  27899  setindregs  35658  dfon2lem6  36367  finminlem  36939  onint1  37070  poimirlem4  38375  ordnexbtwnsuc  44110  gneispace  44976