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

Theorem nsyli 156
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 149 . 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  5893  onssneli  5981  tz7.48-2  7691  tz7.49  7694  php  8301  nndomo  8311  elirrv  8658  setind  8775  zorn2lem3  9523  alephval2  9597  inar1  9800  dfon2lem6  32030  sltres  32153  finminlem  32650  onint1  32786  poimirlem4  33747  gneispace  38959
  Copyright terms: Public domain W3C validator