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  4402  ovrcl  6651  tfi  7015  limom  7042  oaabs2  7685  ecexr  7707  elpmi  7836  elmapex  7838  pmresg  7845  pmsspw  7852  ixpssmap2g  7897  ixpssmapg  7898  resixpfo  7906  infensuc  8098  pm54.43lem  8785  alephnbtwn  8854  cfpwsdom  9366  elbasfv  15860  elbasov  15861  restsspw  16032  homarcl  16618  isipodrs  17101  grpidval  17200  efgrelexlema  18102  subcmn  18182  dvdsrval  18585  mvrf1  19365  pf1rcl  19653  elocv  19952  matrcl  20158  restrcl  20901  ssrest  20920  iscnp2  20983  isfcls  21753  isnghm  22467  dchrrcl  24899  eleenn  25710  hmdmadj  28687  indispconn  30977  cvmtop1  31003  cvmtop2  31004  mrsub0  31174  mrsubf  31175  mrsubccat  31176  mrsubcn  31177  mrsubco  31179  mrsubvrs  31180  msubf  31190  mclsrcl  31219  dfon2lem7  31448  sltval2  31563  sltres  31571  funpartlem  31744  rankeq1o  31973  atbase  34095  llnbase  34314  lplnbase  34339  lvolbase  34383  lhpbase  34803  mapco2g  36796
 Copyright terms: Public domain W3C validator