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

Theorem nsyl2 141
Description: A negated syllogism inference. (Contributed by NM, 26-Jun-1994.) (Proof shortened by Wolf Lammen, 14-Nov-2023.)
Hypotheses
Ref Expression
nsyl2.1 (𝜑 → ¬ 𝜓)
nsyl2.2 𝜒𝜓)
Assertion
Ref Expression
nsyl2 (𝜑𝜒)

Proof of Theorem nsyl2
StepHypRef Expression
1 nsyl2.1 . . 3 (𝜑 → ¬ 𝜓)
2 nsyl2.2 . . 3 𝜒𝜓)
31, 2nsyl3 138 . 2 𝜒 → ¬ 𝜑)
43con4i 114 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:  con1i  147  oprcl  4898  epelg  5584  elfvdm  6942  ovrcl  7473  elfvov1  7474  elfvov2  7475  tfi  7875  limom  7904  oaabs2  8688  ecexr  8751  elpmi  8887  elmapex  8889  pmresg  8911  pmsspw  8918  ixpssmap2g  8968  ixpssmapg  8969  resixpfo  8977  infensuc  9196  pm54.43lem  10041  alephnbtwn  10112  cfpwsdom  10625  elbasfv  17254  elbasov  17255  restsspw  17477  homarcl  18074  isipodrs  18583  grpidval  18675  efgrelexlema  19768  subcmn  19856  dvdsrval  20362  elocv  21687  mvrf1  22007  pf1rcl  22354  matrcl  22417  restrcl  23166  ssrest  23185  iscnp2  23248  isfcls  24018  isnghm  24745  dchrrcl  27285  sltval2  27702  sltres  27708  clwwlknnn  30053  hmdmadj  31960  indispconn  35240  cvmtop1  35266  cvmtop2  35267  mrsub0  35522  mrsubf  35523  mrsubccat  35524  mrsubcn  35525  mrsubco  35527  mrsubvrs  35528  msubf  35538  mclsrcl  35567  dfon2lem7  35791  funpartlem  35944  rankeq1o  36173  bj-brrelex12ALT  37069  bj-fvimacnv0  37288  atbase  39291  llnbase  39512  lplnbase  39537  lvolbase  39581  lhpbase  40001  mapco2g  42730
  Copyright terms: Public domain W3C validator