Theorem nsyl3 139

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 137	1 ⊢ (𝜒 → ¬ 𝜑)

This proof depends on syntax axioms:  ¬ wn 3   → wi 4

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This theorem is used by:  con2i  140  nsyl  141  nsyl2  142  pm2.65i  196  pwnss  5312  reusv2lem2  5360  reldmtpos  8251  tz7.49  8455  omopthlem2  8669  domnsym  9122  sdomirr  9133  infensuc  9174  domnsymfi  9215  fofinf1o  9321  elfi2  9406  sucprcreg  9600  infdifsn  9658  carden2b  10048  alephsucdom  10158  infdif2  10287  fin4i  10376  fin45  10470  bitsf1  16616  pcmpt2  17071  symgvalstruct  19611  ufinffr  24248  eldmgm  27349  lgamucov  27365  facgam  27393  chtub  27539  cuteq1  28203  cofcutr  28310  lfgrnloop  29703  umgredgnlp  29725  clwwlkn0  30619  eupth2lem1  30819  rtelextdg2lem  34358  oddpwdc  34986  bnj1312  35688  erdszelem10  35965  heiborlem1  38746  osumcllem4N  41017  pexmidlem1N  41028  fimgmcyc  43599  fphpd  43823  0nodd  49267