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

Theorem nsyli 154
 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 147 . 2 (𝜑 → (¬ 𝜒 → ¬ 𝜓))
41, 3syl5 33 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  2795  tz7.7  5666  onssneli  5754  tz7.48-2  7424  tz7.49  7427  php  8029  nndomo  8039  elirrv  8387  setind  8493  zorn2lem3  9203  alephval2  9273  inar1  9476  dfon2lem6  30937  sltres  31061  finminlem  31482  onint1  31618  poimirlem4  32583  gneispace  37452
 Copyright terms: Public domain W3C validator