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

Theorem nsyl2 142
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 140 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  144  con4iOLD  145  oprcl  4400  ovrcl  6640  tfi  7001  limom  7028  oaabs2  7671  ecexr  7693  elpmi  7821  elmapex  7823  pmresg  7830  pmsspw  7837  ixpssmap2g  7882  ixpssmapg  7883  resixpfo  7891  infensuc  8083  pm54.43lem  8770  alephnbtwn  8839  cfpwsdom  9351  elbasfv  15836  elbasov  15837  restsspw  16008  homarcl  16594  isipodrs  17077  grpidval  17176  efgrelexlema  18078  subcmn  18158  dvdsrval  18561  mvrf1  19339  pf1rcl  19627  elocv  19926  matrcl  20132  restrcl  20866  ssrest  20885  iscnp2  20948  isfcls  21718  isnghm  22432  dchrrcl  24860  eleenn  25671  hmdmadj  28639  indispconn  30916  cvmtop1  30942  cvmtop2  30943  mrsub0  31113  mrsubf  31114  mrsubccat  31115  mrsubcn  31116  mrsubco  31118  mrsubvrs  31119  msubf  31129  mclsrcl  31158  dfon2lem7  31383  sltval2  31498  sltres  31506  funpartlem  31664  rankeq1o  31893  atbase  34023  llnbase  34242  lplnbase  34267  lvolbase  34311  lhpbase  34731  mapco2g  36724
  Copyright terms: Public domain W3C validator