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  1414  tbw-bijust  1473  tbw-negdf  1474  tbw-ax2  1476  merco1  1488  ax12b  1704  ax11dgen  1740  19.38  1816  nfimdOLD  1832  hbimdOLD  1839  hbimOLD  1841  a16gOLD  2058  stdpc4  2101  sbi2  2144  ax11v  2183  ax11  2243  ax46to4  2251  ax467to4  2258  ax11f  2280  ax11eq  2281  ax11el  2282  ax11indi  2284  ax11indalem  2285  ax11inda2ALT  2286  ax11inda2  2287  morimv  2340  euim  2342  alral  2775  r19.12  2830  r19.27av  2855  r19.37  2868  eqvinc  3076  rr19.3v  3090  class2seteq  4411  dvdemo2  4443  dfwe2  4807  ordunisuc2  4869  tfindsg  4885  findsg  4917  asymref2  5299  iotanul  5483  sorpssuni  6585  sorpssint  6586  smo11  6679  omex  7651  r111  7754  kmlem12  8096  fin1a2lem10  8344  domtriomlem  8377  ltlen  9230  squeeze0  9968  elnnnn0b  10319  iccneg  11073  hash2prde  11743  algcvgblem  13123  prmirred  16811  cxpcn2  20666  bpos1  21103  usgra2edg  21438  nbgra0nb  21477  nbcusgra  21508  wlkdvspthlem  21643  usgrcyclnl2  21664  4cycl4dv  21690  2bornot2b  21794  stcltr2i  23814  mdsl1i  23860  eqvincg  23999  prsiga  24744  rpdmgm  25069  hbimtg  25694  idinside  26278  tb-ax2  26389  wl-jarri  26472  a1i4  26566  tsim3  26981  prtlem1  27029  ax4567to4  27914  ax4567to5  27915  ax4567to6  27916  ax4567to7  27917  cshwssizelem1a  28633  cshwssizelem3  28636  cshwssizelem4a  28637  nbhashuvtx1  28751  frgra3vlem2  28785  frgranbnb  28804  frgrancvvdeqlem2  28814  pm2.43bgbi  28994  pm2.43cbi  28995  hbimpg  29036  hbimpgVD  29413  a9e2ndeqVD  29418  a9e2ndeqALT  29440  bnj1533  29620  bnj1176  29771  a16gNEW7  29943  stdpc4NEW7  29952  sbi2NEW7  29961  ax11vNEW7  29992  atpsubN  30946
  Copyright terms: Public domain W3C validator