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  5349  reusv2lem2  5397  reldmtpos  8216  tz7.49  8442  omopthlem2  8656  domnsym  9096  sdomirr  9111  infensuc  9152  domnsymfi  9200  fofinf1o  9324  elfi2  9406  infdifsn  9649  carden2b  9959  alephsucdom  10071  infdif2  10202  fin4i  10290  fin45  10384  bitsf1  16384  pcmpt2  16823  symgvalstruct  19259  symgvalstructOLD  19260  ufinffr  23425  eldmgm  26516  lgamucov  26532  facgam  26560  chtub  26705  cuteq1  27324  cofcutr  27401  lfgrnloop  28375  umgredgnlp  28397  clwwlkn0  29271  eupth2lem1  29461  oddpwdc  33342  bnj1312  34058  erdszelem10  34180  heiborlem1  36668  osumcllem4N  38819  pexmidlem1N  38830  fphpd  41540  0nodd  46567