MPE Home 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  4821  epelg  5459  elfvdm  6695  ovrcl  7186  tfi  7557  limom  7584  oaabs2  8261  ecexr  8283  elpmi  8414  elmapex  8416  pmresg  8423  pmsspw  8430  ixpssmap2g  8479  ixpssmapg  8480  resixpfo  8488  infensuc  8683  pm54.43lem  9416  alephnbtwn  9485  cfpwsdom  9994  elbasfv  16532  elbasov  16533  restsspw  16693  homarcl  17276  isipodrs  17759  grpidval  17859  efgrelexlema  18804  subcmn  18886  dvdsrval  19324  mvrf1  20133  pf1rcl  20440  elocv  20740  matrcl  20949  restrcl  21693  ssrest  21712  iscnp2  21775  isfcls  22545  isnghm  23259  dchrrcl  25743  clwwlknnn  27738  hmdmadj  29644  indispconn  32378  cvmtop1  32404  cvmtop2  32405  mrsub0  32660  mrsubf  32661  mrsubccat  32662  mrsubcn  32663  mrsubco  32665  mrsubvrs  32666  msubf  32676  mclsrcl  32705  dfon2lem7  32931  sltval2  33060  sltres  33066  funpartlem  33300  rankeq1o  33529  bj-brrelex12ALT  34253  bj-fvimacnv0  34456  atbase  36305  llnbase  36525  lplnbase  36550  lvolbase  36594  lhpbase  37014  mapco2g  39189
  Copyright terms: Public domain W3C validator