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  5339  reusv2lem2  5387  reldmtpos  8214  tz7.49  8440  omopthlem2  8655  domnsym  9095  sdomirr  9110  infensuc  9151  domnsymfi  9199  fofinf1o  9323  elfi2  9405  infdifsn  9648  carden2b  9958  alephsucdom  10070  infdif2  10201  fin4i  10289  fin45  10383  bitsf1  16384  pcmpt2  16825  symgvalstruct  19306  symgvalstructOLD  19307  ufinffr  23755  eldmgm  26870  lgamucov  26886  facgam  26914  chtub  27061  cuteq1  27682  cofcutr  27760  lfgrnloop  28854  umgredgnlp  28876  clwwlkn0  29750  eupth2lem1  29940  oddpwdc  33842  bnj1312  34558  erdszelem10  34680  heiborlem1  37169  osumcllem4N  39320  pexmidlem1N  39331  fphpd  42043  0nodd  47033