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

Theorem nsyl 135
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 133 . 2 (𝜒 → ¬ 𝜑)
43con2i 134 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  150  intnand  1000  intnanrd  1001  intn3an1d  1591  intn3an2d  1592  intn3an3d  1593  camestres  2708  camestros  2712  calemes  2719  calemos  2722  pssn2lp  3850  sotrieq  5214  ordnbtwn  5977  ordnbtwnOLD  5978  funun  6093  canth  6772  dfwe2  7147  opabn1stprc  7396  pwuninel2  7570  swoer  7943  swoord1  7944  swoord2  7945  php2  8312  en3lp  8684  cantnfp1lem1  8750  cantnfp1lem3  8752  cantnflem2  8762  rankxpsuc  8920  cardmin2  9034  infxpenlem  9046  cardaleph  9122  isfin4-3  9349  fin23lem24  9356  fin23lem25  9358  fin23lem26  9359  fin23lem38  9383  isfin32i  9399  fin34  9424  fin67  9429  nd3  9623  fpwwe2lem13  9676  canthnum  9683  canthwe  9685  pwfseq  9698  gchcdaidm  9702  gchxpidm  9703  r1wunlim  9771  suplem2pr  10087  elnnz  11599  fzneuz  12634  fzodisj  12716  fzodisjsn  12720  hasheq0  13366  swrd0  13654  cnpart  14199  sqreulem  14318  rlimuni  14500  rlimcld2  14528  divalglem6  15343  bitsf1  15390  infpnlem1  15836  ramubcl  15944  ressress  16160  mreexmrid  16525  gsum2d  18591  dprddomprc  18619  ablfacrplem  18684  rng1nfld  19500  mplsubrglem  19661  mdetunilem6  20645  mdetunilem9  20648  madugsum  20671  infil  21888  fbasfip  21893  fgcl  21903  fin1aufil  21957  hauspwpwf1  22012  ovolicc2lem4  23508  ovolioo  23556  i1fima2sn  23666  itg1addlem4  23685  itgsplitioo  23823  lhop1lem  23995  chordthmlem  24779  ressatans  24881  ftalem5  25023  ppiprm  25097  chtprm  25099  lgsdir2lem2  25271  dirith2  25437  axlowdimlem13  26054  axlowdim1  26059  nfrgr2v  27447  eulerpartlemgvv  30768  ballotlemfp1  30883  ballotlem4  30890  ballotlemirc  30923  erdszelem8  31508  bccolsum  31953  noresle  32173  noetalem3  32192  nn0prpwlem  32644  nn0prpw  32645  ivthALT  32657  nandsym1  32748  onsucsuccmpi  32769  onint1  32775  topdifinffinlem  33524  relowlssretop  33540  fin2solem  33726  poimirlem2  33742  poimirlem3  33743  poimirlem4  33744  poimirlem6  33746  poimirlem7  33747  poimirlem8  33748  poimirlem9  33749  poimirlem13  33753  poimirlem14  33754  poimirlem15  33755  poimirlem16  33756  poimirlem17  33757  poimirlem19  33759  poimirlem20  33760  poimirlem21  33761  poimirlem22  33762  poimirlem23  33763  poimirlem26  33766  poimirlem31  33771  mblfinlem1  33777  mblfinlem2  33778  dvasin  33827  dvacos  33828  areacirclem4  33834  ax10fromc7  34702  hdmaplem1  37580  hdmaplem2N  37581  hdmaplem3  37582  irrapx1  37912  gneispace  38952  sineq0ALT  39690  sumnnodd  40383  fperdvper  40654  stoweidlem35  40773  stirlinglem5  40816  fourierdlem68  40912  fourierswlem  40968  fouriersw  40969  zrninitoringc  42599  lmod1zrnlvec  42811  elsetrecslem  42973
  Copyright terms: Public domain W3C validator