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  5322  reusv2lem2  5370  reldmtpos  8226  tz7.49  8428  omopthlem2  8642  domnsym  9087  sdomirr  9098  infensuc  9139  domnsymfi  9180  fofinf1o  9285  elfi2  9370  sucprcreg  9564  infdifsn  9622  carden2b  9958  alephsucdom  10068  infdif2  10197  fin4i  10286  fin45  10380  bitsf1  16508  pcmpt2  16957  symgvalstruct  19471  ufinffr  24095  eldmgm  27195  lgamucov  27211  facgam  27239  chtub  27385  cuteq1  28019  cofcutr  28126  lfgrnloop  29484  umgredgnlp  29506  clwwlkn0  30388  eupth2lem1  30578  rtelextdg2lem  34125  oddpwdc  34753  bnj1312  35455  erdszelem10  35700  heiborlem1  38490  osumcllem4N  40761  pexmidlem1N  40772  fimgmcyc  43330  fphpd  43571  0nodd  48963