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

Theorem nsyli 160
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 155 . 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  3020  tz7.7  6190  onssneli  6273  tz7.48-2  8053  tz7.49  8056  php  8677  nndomog  8684  elirrv  9036  setind  9152  zorn2lem3  9897  alephval2  9971  inar1  10174  dfon2lem6  33040  sltres  33176  finminlem  33673  onint1  33804  poimirlem4  34939  gneispace  40619
  Copyright terms: Public domain W3C validator