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

Theorem nsyl2 140
Description: A negated syllogism inference. (Contributed by NM, 26-Jun-1994.)
Hypotheses
Ref Expression
nsyl2.1 (𝜑 → ¬ 𝜓)
nsyl2.2 𝜒𝜓)
Assertion
Ref Expression
nsyl2 (𝜑𝜒)

Proof of Theorem nsyl2
StepHypRef Expression
1 nsyl2.1 . 2 (𝜑 → ¬ 𝜓)
2 nsyl2.2 . . 3 𝜒𝜓)
32a1i 11 . 2 (𝜑 → (¬ 𝜒𝜓))
41, 3mt3d 138 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  142  con4iOLD  143  oprcl  4359  ovrcl  6562  tfi  6922  limom  6949  oaabs2  7589  ecexr  7611  elpmi  7739  elmapex  7741  pmresg  7748  pmsspw  7755  ixpssmap2g  7800  ixpssmapg  7801  resixpfo  7809  infensuc  8000  pm54.43lem  8685  alephnbtwn  8754  cfpwsdom  9262  elbasfv  15694  elbasov  15695  restsspw  15861  homarcl  16447  isipodrs  16930  grpidval  17029  efgrelexlema  17931  subcmn  18011  dvdsrval  18414  mvrf1  19192  pf1rcl  19480  elocv  19773  matrcl  19979  restrcl  20713  ssrest  20732  iscnp2  20795  isfcls  21565  isnghm  22269  dchrrcl  24682  eleenn  25494  hmdmadj  27989  indispcon  30276  cvmtop1  30302  cvmtop2  30303  mrsub0  30473  mrsubf  30474  mrsubccat  30475  mrsubcn  30476  mrsubco  30478  mrsubvrs  30479  msubf  30489  mclsrcl  30518  dfon2lem7  30744  sltval2  30859  sltres  30867  funpartlem  31025  rankeq1o  31254  atbase  33390  llnbase  33609  lplnbase  33634  lvolbase  33678  lhpbase  34098  mapco2g  36091
  Copyright terms: Public domain W3C validator