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  2952  tz7.7  6409  onssneli  6499  tz7.48-2  8483  tz7.49  8486  php  9248  phpOLD  9260  nndomogOLD  9264  elirrv  9637  setind  9775  zorn2lem3  10539  alephval2  10613  inar1  10816  sltres  27708  dfon2lem6  35790  finminlem  36320  onint1  36451  poimirlem4  37632  ordnexbtwnsuc  43285  gneispace  44152
  Copyright terms: Public domain W3C validator