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

Theorem nsyl2 145
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 143 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  147  oprcl  4662  elfvdm  6478  ovrcl  6962  tfi  7331  limom  7358  oaabs2  8009  ecexr  8031  elpmi  8159  elmapex  8161  pmresg  8168  pmsspw  8175  ixpssmap2g  8223  ixpssmapg  8224  resixpfo  8232  infensuc  8426  pm54.43lem  9158  alephnbtwn  9227  cfpwsdom  9741  elbasfv  16316  elbasov  16317  restsspw  16478  homarcl  17063  isipodrs  17547  grpidval  17646  efgrelexlema  18548  subcmn  18628  dvdsrval  19032  mvrf1  19822  pf1rcl  20109  elocv  20411  matrcl  20622  restrcl  21369  ssrest  21388  iscnp2  21451  isfcls  22221  isnghm  22935  dchrrcl  25417  eleenn  26245  clwwlknnn  27422  hmdmadj  29371  indispconn  31815  cvmtop1  31841  cvmtop2  31842  mrsub0  32012  mrsubf  32013  mrsubccat  32014  mrsubcn  32015  mrsubco  32017  mrsubvrs  32018  msubf  32028  mclsrcl  32057  dfon2lem7  32282  sltval2  32398  sltres  32404  funpartlem  32638  rankeq1o  32867  atbase  35438  llnbase  35658  lplnbase  35683  lvolbase  35727  lhpbase  36147  mapco2g  38230
  Copyright terms: Public domain W3C validator