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  5317  reusv2lem2  5365  reldmtpos  8276  tz7.49  8480  omopthlem2  8694  domnsym  9147  sdomirr  9158  infensuc  9199  domnsymfi  9240  fofinf1o  9346  elfi2  9430  sucprcreg  9624  infdifsn  9682  carden2b  10072  alephsucdom  10182  infdif2  10311  fin4i  10400  fin45  10494  bitsf1  16642  pcmpt2  17097  symgvalstruct  19638  ufinffr  24275  eldmgm  27376  lgamucov  27392  facgam  27420  chtub  27566  cuteq1  28230  cofcutr  28337  lfgrnloop  29730  umgredgnlp  29752  clwwlkn0  30646  eupth2lem1  30846  rtelextdg2lem  34425  oddpwdc  35053  bnj1312  35755  erdszelem10  36131  heiborlem1  38936  osumcllem4N  41207  pexmidlem1N  41218  fimgmcyc  43789  fphpd  44014  0nodd  49470