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  5358  reusv2lem2  5405  reldmtpos  8258  tz7.49  8484  omopthlem2  8697  domnsym  9138  sdomirr  9153  infensuc  9194  domnsymfi  9238  fofinf1o  9370  elfi2  9452  infdifsn  9695  carden2b  10005  alephsucdom  10117  infdif2  10247  fin4i  10336  fin45  10430  bitsf1  16480  pcmpt2  16927  symgvalstruct  19429  symgvalstructOLD  19430  ufinffr  23953  eldmgm  27080  lgamucov  27096  facgam  27124  chtub  27271  cuteq1  27893  cofcutr  27973  lfgrnloop  29157  umgredgnlp  29179  clwwlkn0  30057  eupth2lem1  30247  rtelextdg2lem  33732  oddpwdc  34336  bnj1312  35051  erdszelem10  35185  heiborlem1  37798  osumcllem4N  39942  pexmidlem1N  39953  fimgmcyc  42521  fphpd  42804  0nodd  48014