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  5215  reusv2lem2  5265  reldmtpos  7883  tz7.49  8064  omopthlem2  8266  domnsym  8627  sdomirr  8638  infensuc  8679  fofinf1o  8783  elfi2  8862  infdifsn  9104  carden2b  9380  alephsucdom  9490  infdif2  9621  fin4i  9709  fin45  9803  bitsf1  15785  pcmpt2  16219  symgvalstruct  18517  ufinffr  22534  eldmgm  25607  lgamucov  25623  facgam  25651  chtub  25796  lfgrnloop  26918  umgredgnlp  26940  clwwlkn0  27813  eupth2lem1  28003  oddpwdc  31722  bnj1312  32440  erdszelem10  32560  heiborlem1  35249  osumcllem4N  37255  pexmidlem1N  37266  fphpd  39757  0nodd  44430