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

Theorem nsyl2 143
 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 140 . 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  149  oprcl  4828  epelg  5465  elfvdm  6701  ovrcl  7196  tfi  7567  limom  7594  oaabs2  8271  ecexr  8293  elpmi  8424  elmapex  8426  pmresg  8433  pmsspw  8440  ixpssmap2g  8490  ixpssmapg  8491  resixpfo  8499  infensuc  8694  pm54.43lem  9427  alephnbtwn  9496  cfpwsdom  10005  elbasfv  16543  elbasov  16544  restsspw  16704  homarcl  17287  isipodrs  17770  grpidval  17870  efgrelexlema  18874  subcmn  18956  dvdsrval  19394  mvrf1  20204  pf1rcl  20511  elocv  20811  matrcl  21020  restrcl  21764  ssrest  21783  iscnp2  21846  isfcls  22616  isnghm  23331  dchrrcl  25815  clwwlknnn  27810  hmdmadj  29716  indispconn  32481  cvmtop1  32507  cvmtop2  32508  mrsub0  32763  mrsubf  32764  mrsubccat  32765  mrsubcn  32766  mrsubco  32768  mrsubvrs  32769  msubf  32779  mclsrcl  32808  dfon2lem7  33034  sltval2  33163  sltres  33169  funpartlem  33403  rankeq1o  33632  bj-brrelex12ALT  34358  bj-fvimacnv0  34567  atbase  36424  llnbase  36644  lplnbase  36669  lvolbase  36713  lhpbase  37133  mapco2g  39311
 Copyright terms: Public domain W3C validator