Theorem nsyl3 138

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 136	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  139  nsyl  140  nsyl2  141  pwnss  5350  reusv2lem2  5398  reldmtpos  8223  tz7.49  8449  omopthlem2  8663  domnsym  9103  sdomirr  9118  infensuc  9159  domnsymfi  9207  fofinf1o  9331  elfi2  9413  infdifsn  9656  carden2b  9966  alephsucdom  10078  infdif2  10209  fin4i  10297  fin45  10391  bitsf1  16393  pcmpt2  16832  symgvalstruct  19307  symgvalstructOLD  19308  ufinffr  23655  eldmgm  26760  lgamucov  26776  facgam  26804  chtub  26949  cuteq1  27569  cofcutr  27647  lfgrnloop  28650  umgredgnlp  28672  clwwlkn0  29546  eupth2lem1  29736  oddpwdc  33649  bnj1312  34365  erdszelem10  34487  heiborlem1  36984  osumcllem4N  39135  pexmidlem1N  39146  fphpd  41858  0nodd  46848