MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  nsyli Structured version   Visualization version   GIF version

Theorem nsyli 157
Description: A negated syllogism inference. (Contributed by NM, 3-May-1994.)
Hypotheses
Ref Expression
nsyli.1 (𝜑 → (𝜓𝜒))
nsyli.2 (𝜃 → ¬ 𝜒)
Assertion
Ref Expression
nsyli (𝜑 → (𝜃 → ¬ 𝜓))

Proof of Theorem nsyli
StepHypRef Expression
1 nsyli.2 . 2 (𝜃 → ¬ 𝜒)
2 nsyli.1 . . 3 (𝜑 → (𝜓𝜒))
32con3d 152 . 2 (𝜑 → (¬ 𝜒 → ¬ 𝜓))
41, 3syl5 34 1 (𝜑 → (𝜃 → ¬ 𝜓))
Colors of variables: wff setvar class
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:  necon3ad  2956  tz7.7  6292  onssneli  6376  tz7.48-2  8273  tz7.49  8276  php  8993  phpOLD  9005  nndomogOLD  9009  elirrv  9355  setind  9492  zorn2lem3  10254  alephval2  10328  inar1  10531  dfon2lem6  33764  sltres  33865  finminlem  34507  onint1  34638  poimirlem4  35781  gneispace  41744
  Copyright terms: Public domain W3C validator