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  2951  tz7.7  6412  onssneli  6502  tz7.48-2  8481  tz7.49  8484  php  9245  phpOLD  9257  nndomogOLD  9261  elirrv  9634  setind  9772  zorn2lem3  10536  alephval2  10610  inar1  10813  sltres  27722  dfon2lem6  35770  finminlem  36301  onint1  36432  poimirlem4  37611  ordnexbtwnsuc  43257  gneispace  44124