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  4263  ovrcl  6460  tfi  6820  limom  6847  oaabs2  7487  ecexr  7509  elpmi  7637  elmapex  7639  pmresg  7646  pmsspw  7653  ixpssmap2g  7698  ixpssmapg  7699  resixpfo  7707  infensuc  7898  pm54.43lem  8583  alephnbtwn  8652  cfpwsdom  9160  elbasfv  15630  elbasov  15631  restsspw  15797  homarcl  16391  isipodrs  16874  grpidval  16973  efgrelexlema  17891  subcmn  17970  dvdsrval  18373  mvrf1  19148  pf1rcl  19436  elocv  19732  matrcl  19938  restrcl  20672  ssrest  20691  iscnp2  20754  isfcls  21524  isnghm  22228  isnghmOLD  22246  dchrrcl  24655  eleenn  25467  hmdmadj  27972  indispcon  30316  cvmtop1  30342  cvmtop2  30343  mrsub0  30513  mrsubf  30514  mrsubccat  30515  mrsubcn  30516  mrsubco  30518  mrsubvrs  30519  msubf  30529  mclsrcl  30558  dfon2lem7  30781  sltval2  30889  sltres  30897  funpartlem  31055  rankeq1o  31284  atbase  33469  llnbase  33688  lplnbase  33713  lvolbase  33757  lhpbase  34177  mapco2g  36170
 Copyright terms: Public domain W3C validator