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

Axiom ax-1 7
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  ph and  ps to the assertion of  ph simply." (Contributed by NM, 5-Aug-1993.)
Assertion
Ref Expression
ax-1  |-  ( ph  ->  ( ps  ->  ph )
)

Detailed syntax breakdown of Axiom ax-1
StepHypRef Expression
1 wph . 2  wff  ph
2 wps . . 3  wff  ps
32, 1wi 6 . 2  wff  ( ps 
->  ph )
41, 3wi 6 1  wff  ( ph  ->  ( ps  ->  ph )
)
Colors of variables: wff set class
This axiom is referenced by:  a1i  12  id  21  id1  22  a1d  24  a1dd  44  jarr  93  pm2.86i  94  pm2.86d  95  pm2.51  147  dfbi1gb  187  pm5.1im  231  biimt  327  pm5.4  353  pm4.8  356  olc  375  simpl  445  pm4.45im  547  pm2.64  767  pm2.74  822  pm2.82  828  oibabs  856  pm5.14  861  biort  871  dedlem0a  923  meredith  1400  tbw-bijust  1458  tbw-negdf  1459  tbw-ax2  1461  merco1  1473  ax12o10lem7  1641  ax12o10lem11  1645  a16gALT  1679  hbim  1723  nfimd  1727  ax46to4  1747  ax467to4  1753  hbimd  1809  stdpc4  1897  ax11  1942  sbi2  1957  ax11v  1991  ax11eq  2108  ax11el  2109  ax11f  2110  ax11indi  2112  ax11indalem  2113  ax11inda2ALT  2114  ax11inda2  2115  moimv  2164  euim  2166  alral  2574  r19.12  2629  r19.27av  2654  r19.37  2662  eqvinc  2863  rr19.3v  2877  class2seteq  4137  dvdemo2  4169  dfwe2  4531  ordunisuc2  4593  tfindsg  4609  findsg  4641  asymref2  5034  sorpssuni  6206  sorpssint  6207  iotanul  6226  smo11  6335  omex  7298  r111  7401  kmlem12  7741  fin1a2lem10  7989  domtriomlem  8022  ltlen  8876  squeeze0  9613  elnnnn0b  9961  iccneg  10709  algcvgblem  12695  prmirred  16396  cxpcn2  20034  bpos1  20470  2bornot2b  20783  stcltr2i  22801  mdsl1i  22847  hbimtg  23518  idinside  24068  tb-ax2  24179  wl-jarri  24262  inttarcar  25254  a1i4  25554  prtlem1  26060  ax4567to4  26955  ax4567to5  26956  ax4567to6  26957  ax4567to7  26958  stoweidlem4  27074  aibnbna  27149  pm2.43bgbi  27316  pm2.43cbi  27317  hbimpg  27357  hbimpgVD  27714  a9e2ndeqVD  27719  a9e2ndeqALT  27742  bnj1533  27917  bnj1176  28068  ax11dgenK  28175  ax12o10lem7K  28193  ax12o10lem7X  28194  ax12o10lem11K  28201  ax12o10lem11X  28202  a16gALTX  28249  a12study11  28289  a12study11n  28290  ax9lem9  28299  ax9lem10  28300  atpsubN  29093
  Copyright terms: Public domain W3C validator