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  5290  reusv2lem2  5338  reldmtpos  8179  tz7.49  8379  omopthlem2  8591  domnsym  9036  sdomirr  9047  infensuc  9088  domnsymfi  9129  fofinf1o  9237  elfi2  9322  sucprcreg  9515  infdifsn  9573  carden2b  9886  alephsucdom  9996  infdif2  10126  fin4i  10215  fin45  10309  bitsf1  16410  pcmpt2  16859  symgvalstruct  19367  ufinffr  23908  eldmgm  27003  lgamucov  27019  facgam  27047  chtub  27193  cuteq1  27827  cofcutr  27934  lfgrnloop  29212  umgredgnlp  29234  clwwlkn0  30117  eupth2lem1  30307  rtelextdg2lem  33890  oddpwdc  34518  bnj1312  35220  erdszelem10  35402  heiborlem1  38150  osumcllem4N  40423  pexmidlem1N  40434  fimgmcyc  42997  fphpd  43266  0nodd  48662