Theorem nsyl3 132

Description: A negated syllogism inference. (Contributed by NM, 1-Dec-1995.)

Hypotheses

Ref	Expression
nsyl3.1	⊢ (𝜑 → ¬ 𝜓)
nsyl3.2	⊢ (𝜒 → 𝜓)

Assertion

Ref	Expression
nsyl3	⊢ (𝜒 → ¬ 𝜑)

Proof of Theorem nsyl3

Step	Hyp	Ref	Expression
1		nsyl3.2	. 2 ⊢ (𝜒 → 𝜓)
2		nsyl3.1	. . 3 ⊢ (𝜑 → ¬ 𝜓)
3	2	a1i 11	. 2 ⊢ (𝜒 → (𝜑 → ¬ 𝜓))
4	1, 3	mt2d 130	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:  con2i  133  nsyl  134  cesare  2557  cesaro  2561  pwnss  4756  reusv2lem2  4795  reusv2lem2OLD  4796  reldmtpos  7247  tz7.49  7427  omopthlem2  7623  domnsym  7971  sdomirr  7982  infensuc  8023  fofinf1o  8126  elfi2  8203  infdifsn  8437  carden2b  8676  alephsucdom  8785  infdif2  8915  fin4i  9003  bitsf1  15006  pcmpt2  15435  ufinffr  21543  eldmgm  24548  lgamucov  24564  facgam  24592  chtub  24737  lfgrnloop  25791  umgredgnlp  25818  eupath2lem1  26504  oddpwdc  29743  bnj1312  30380  erdszelem10  30436  heiborlem1  32780  osumcllem4N  34263  pexmidlem1N  34274  fphpd  36398  eupth2lem1  41386  0nodd  41600