Theorem nsyli 160

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 155	. 2 ⊢ (𝜑 → (¬ 𝜒 → ¬ 𝜓))
4	1, 3	syl5 34	1 ⊢ (𝜑 → (𝜃 → ¬ 𝜓))

Syntax hints:  ¬ wn 3   → wi 4

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This theorem is referenced by:  necon3ad  3029  tz7.7  6217  onssneli  6300  tz7.48-2  8078  tz7.49  8081  php  8701  nndomo  8712  elirrv  9060  setind  9176  zorn2lem3  9920  alephval2  9994  inar1  10197  dfon2lem6  33033  sltres  33169  finminlem  33666  onint1  33797  poimirlem4  34911  nndomog  39917  gneispace  40504