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  5316  reusv2lem2  5364  reldmtpos  8237  tz7.49  8441  omopthlem2  8655  domnsym  9108  sdomirr  9119  infensuc  9160  domnsymfi  9201  fofinf1o  9306  elfi2  9391  sucprcreg  9585  infdifsn  9643  carden2b  9997  alephsucdom  10107  infdif2  10236  fin4i  10325  fin45  10419  bitsf1  16561  pcmpt2  17010  symgvalstruct  19550  ufinffr  24187  eldmgm  27290  lgamucov  27306  facgam  27334  chtub  27480  cuteq1  28114  cofcutr  28221  lfgrnloop  29614  umgredgnlp  29636  clwwlkn0  30530  eupth2lem1  30730  rtelextdg2lem  34269  oddpwdc  34898  bnj1312  35600  erdszelem10  35862  heiborlem1  38626  osumcllem4N  40897  pexmidlem1N  40908  fimgmcyc  43481  fphpd  43722  0nodd  49150