Theorem nsyl3 140

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 138	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  141  nsyl  142  nsyl2  143  pwnss  5216  reusv2lem2  5266  reldmtpos  7929  tz7.49  8110  omopthlem2  8314  domnsym  8693  sdomirr  8704  infensuc  8745  fofinf1o  8872  elfi2  8951  infdifsn  9193  carden2b  9469  alephsucdom  9579  infdif2  9710  fin4i  9798  fin45  9892  bitsf1  15889  pcmpt2  16329  symgvalstruct  18643  ufinffr  22680  eldmgm  25759  lgamucov  25775  facgam  25803  chtub  25948  lfgrnloop  27070  umgredgnlp  27092  clwwlkn0  27965  eupth2lem1  28155  oddpwdc  31891  bnj1312  32609  erdszelem10  32733  cofcutr  33730  heiborlem1  35592  osumcllem4N  37596  pexmidlem1N  37607  fphpd  40210  0nodd  44898