Theorem nsyl3 133

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 131	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  134  nsyl  135  cesare  2569  cesaro  2573  pwnss  4830  reusv2lem2  4869  reusv2lem2OLD  4870  reldmtpos  7360  tz7.49  7540  omopthlem2  7736  domnsym  8086  sdomirr  8097  infensuc  8138  fofinf1o  8241  elfi2  8320  infdifsn  8554  carden2b  8793  alephsucdom  8902  infdif2  9032  fin4i  9120  bitsf1  15168  pcmpt2  15597  ufinffr  21733  eldmgm  24748  lgamucov  24764  facgam  24792  chtub  24937  lfgrnloop  26020  umgredgnlp  26042  eupth2lem1  27078  oddpwdc  30416  bnj1312  31126  erdszelem10  31182  heiborlem1  33610  osumcllem4N  35245  pexmidlem1N  35256  fphpd  37380  0nodd  41810