MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  ax-1 Unicode version

Axiom ax-1 6
Description: Axiom Simp. Axiom A1 of [Margaris] p. 49. One of the 3 axioms of propositional calculus. The 3 axioms are also given as Definition 2.1 of [Hamilton] p. 28. This axiom is called Simp or "the principle of simplification" in Principia Mathematica (Theorem *2.02 of [WhiteheadRussell] p. 100) because "it enables us to pass from the joint assertion of and to the assertion of simply." (Contributed by NM, 5-Aug-1993.)
Assertion
Ref Expression
ax-1

Detailed syntax breakdown of Axiom ax-1
StepHypRef Expression
1 wph . 2
2 wps . . 3
32, 1wi 4 . 2
41, 3wi 4 1
Colors of variables: wff set class
This axiom is referenced by:  a1i  11  id  21  id1  22  a1d  24  a1dd  45  jarr  94  pm2.86i  95  pm2.86d  96  pm2.51  148  dfbi1gb  187  pm5.1im  231  biimt  327  pm5.4  353  pm4.8  356  olc  375  simpl  445  pm4.45im  547  pm2.64  766  pm2.74  821  pm2.82  827  oibabs  853  pm5.14  858  biort  868  dedlem0a  920  meredith  1423  tbw-bijust  1482  tbw-negdf  1483  tbw-ax2  1485  merco1  1497  ax13b  1709  ax12dgen  1736  19.38  1810  nfimdOLD  1826  hbimOLD  1834  a16gOLD  2047  stdpc4  2091  sbi2  2135  ax12v  2181  ax12  2257  axc5c7toc5  2265  axc5c711toc5  2272  ax12f  2293  ax12eq  2294  ax12el  2295  ax12indi  2297  ax12indalem  2298  ax12inda2ALT  2299  ax12inda2  2300  morimOLD  2366  morimvOLD  2367  euim  2369  alral  2810  r19.12  2865  r19.27av  2890  r19.37  2903  eqvinc  3113  rr19.3v  3127  class2seteq  4467  dvdemo2  4535  asymref2  5217  iotanul  5395  sorpssuni  6335  sorpssint  6336  dfwe2  6358  ordunisuc2  6420  tfindsg  6436  findsg  6468  smo11  6738  omex  7710  r111  7813  kmlem12  8155  fin1a2lem10  8403  domtriomlem  8436  ltlen  9298  squeeze0  10044  elnnnn0b  10433  iccneg  11211  hash2prde  11971  disjxwrd  12136  algcvgblem  13538  cshwshashlem1  13908  cshwshashlem2  13909  prmirred  17278  cxpcn2  21139  bpos1  21576  usgra2edg  21911  nbgra0nb  21950  nbcusgra  21981  wlkdvspthlem  22116  usgrcyclnl2  22137  4cycl4dv  22163  2bornot2b  22267  stcltr2i  24289  mdsl1i  24335  eqvincg  24474  prsiga  25245  rpdmgm  25648  hbimtg  26264  idinside  26848  tb-ax2  26959  wl-jarri  27069  wl-equsal1t  27082  a1i4  27162  tsim3  27577  prtlem1  27623  axc5c4c711toc5  28505  axc5c4c711toc4  28506  axc5c4c711toc7  28507  axc5c4c711to11  28508  nn01to3  29044  clwwlkgt0  29293  scshwfzeqfzo  29351  nbhashuvtx1  29392  rusgrasn  29416  frgra3vlem2  29452  frgranbnb  29471  frgrancvvdeqlem2  29483  frgrareg  29569  frgraregord013  29570  frgraogt3nreg  29572  hash2pwpr  29595  pm2.43bgbi  29790  pm2.43cbi  29791  hbimpg  29832  hbimpgVD  30209  a6e2ndeqVD  30214  a6e2ndeqALT  30236  bnj1533  30416  bnj1176  30567  bj-andnotim  30635  bj-alax1  30638  bj-equsal1t  30645  a16gNEW11  30821  stdpc4NEW11  30830  sbi2NEW11  30839  ax12vNEW11  30870  atpsubN  31823
  Copyright terms: Public domain W3C validator