Theorem nsyl3 139

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 137	1 ⊢ (𝜒 → ¬ 𝜑)

This proof depends on syntax axioms:  ¬ wn 3   → wi 4

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This theorem is used by:  con2i  140  nsyl  141  nsyl2  142  pm2.65i  196  pwnss  5320  reusv2lem2  5368  reldmtpos  8235  tz7.49  8437  omopthlem2  8651  domnsym  9104  sdomirr  9115  infensuc  9156  domnsymfi  9197  fofinf1o  9302  elfi2  9387  sucprcreg  9581  infdifsn  9639  carden2b  9975  alephsucdom  10085  infdif2  10214  fin4i  10303  fin45  10397  bitsf1  16538  pcmpt2  16987  symgvalstruct  19523  ufinffr  24154  eldmgm  27254  lgamucov  27270  facgam  27298  chtub  27444  cuteq1  28078  cofcutr  28185  lfgrnloop  29566  umgredgnlp  29588  clwwlkn0  30482  eupth2lem1  30682  rtelextdg2lem  34221  oddpwdc  34850  bnj1312  35552  erdszelem10  35764  heiborlem1  38546  osumcllem4N  40817  pexmidlem1N  40828  fimgmcyc  43401  fphpd  43642  0nodd  49070