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

Theorem nsyl 137
Description: A negated syllogism inference. (Contributed by NM, 31-Dec-1993.) (Proof shortened by Wolf Lammen, 2-Mar-2013.)
Hypotheses
Ref Expression
nsyl.1 (𝜑 → ¬ 𝜓)
nsyl.2 (𝜒𝜓)
Assertion
Ref Expression
nsyl (𝜑 → ¬ 𝜒)

Proof of Theorem nsyl
StepHypRef Expression
1 nsyl.1 . . 3 (𝜑 → ¬ 𝜓)
2 nsyl.2 . . 3 (𝜒𝜓)
31, 2nsyl3 135 . 2 (𝜒 → ¬ 𝜑)
43con2i 136 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:  con3i  151  intnand  476  intnanrd  477  intn3an1d  1590  intn3an2d  1591  intn3an3d  1592  camestres  2719  camestros  2723  calemes  2730  calemos  2733  pssn2lp  3858  sotrieq  5197  ordnbtwn  5959  ordnbtwnOLD  5960  funun  6075  canth  6751  dfwe2  7128  opabn1stprc  7377  pwuninel2  7552  swoer  7926  swoord1  7927  swoord2  7928  php2  8301  en3lp  8673  cantnfp1lem1  8739  cantnfp1lem3  8741  cantnflem2  8751  rankxpsuc  8909  cardmin2  9024  infxpenlem  9036  cardaleph  9112  isfin4-3  9339  fin23lem24  9346  fin23lem25  9348  fin23lem26  9349  fin23lem38  9373  isfin32i  9389  fin34  9414  fin67  9419  nd3  9613  fpwwe2lem13  9666  canthnum  9673  canthwe  9675  pwfseq  9688  gchcdaidm  9692  gchxpidm  9693  r1wunlim  9761  suplem2pr  10077  elnnz  11589  fzneuz  12628  fzodisj  12710  fzodisjsn  12714  hasheq0  13356  swrd0  13643  cnpart  14188  sqreulem  14307  rlimuni  14489  rlimcld2  14517  divalglem6  15329  bitsf1  15376  infpnlem1  15821  ramubcl  15929  ressress  16146  mreexmrid  16511  gsum2d  18578  dprddomprc  18607  ablfacrplem  18672  rng1nfld  19493  mplsubrglem  19654  mdetunilem6  20641  mdetunilem9  20644  madugsum  20667  infil  21887  fbasfip  21892  fgcl  21902  fin1aufil  21956  hauspwpwf1  22011  ovolicc2lem4  23508  ovolioo  23556  i1fima2sn  23667  itg1addlem4  23686  itgsplitioo  23824  lhop1lem  23996  chordthmlem  24780  ressatans  24882  ftalem5  25024  ppiprm  25098  chtprm  25100  lgsdir2lem2  25272  dirith2  25438  axlowdimlem13  26055  axlowdim1  26060  nfrgr2v  27454  eulerpartlemgvv  30778  ballotlemfp1  30893  ballotlem4  30900  ballotlemirc  30933  erdszelem8  31518  bccolsum  31963  noresle  32183  noetalem3  32202  nn0prpwlem  32654  nn0prpw  32655  ivthALT  32667  nandsym1  32758  onsucsuccmpi  32779  onint1  32785  topdifinffinlem  33532  relowlssretop  33548  fin2solem  33728  poimirlem2  33744  poimirlem3  33745  poimirlem4  33746  poimirlem6  33748  poimirlem7  33749  poimirlem8  33750  poimirlem9  33751  poimirlem13  33755  poimirlem14  33756  poimirlem15  33757  poimirlem16  33758  poimirlem17  33759  poimirlem19  33761  poimirlem20  33762  poimirlem21  33763  poimirlem22  33764  poimirlem23  33765  poimirlem26  33768  poimirlem31  33773  mblfinlem1  33779  mblfinlem2  33780  dvasin  33828  dvacos  33829  areacirclem4  33835  ax10fromc7  34703  hdmaplem1  37581  hdmaplem2N  37582  hdmaplem3  37583  irrapx1  37918  gneispace  38958  sineq0ALT  39695  sumnnodd  40380  fperdvper  40651  stoweidlem35  40769  stirlinglem5  40812  fourierdlem68  40908  fourierswlem  40964  fouriersw  40965  zrninitoringc  42599  lmod1zrnlvec  42811  elsetrecslem  42973
  Copyright terms: Public domain W3C validator