Theorem nsyli 157

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 152	. 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  2952  tz7.7  6409  onssneli  6499  tz7.48-2  8483  tz7.49  8486  php  9248  phpOLD  9260  nndomogOLD  9264  elirrv  9637  setind  9775  zorn2lem3  10539  alephval2  10613  inar1  10816  sltres  27708  dfon2lem6  35790  finminlem  36320  onint1  36451  poimirlem4  37632  ordnexbtwnsuc  43285  gneispace  44152