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  2969  tz7.7  6388  onssneli  6480  tz7.48-2  8452  tz7.49  8455  php  9222  elirrvOLDOLD  9593  setind  9748  zorn2lem3  10576  alephval2  10657  inar1  10860  ltsres  28019  setindregs  35798  dfon2lem6  36550  finminlem  37106  onint1  37237  poimirlem4  38542  ordnexbtwnsuc  44268  gneispace  45133