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  1896  ax11  1941  sbi2  1956  ax11v  1990  ax11eq  2105  ax11el  2106  ax11f  2107  ax11indi  2109  ax11indalem  2110  ax11inda2ALT  2111  ax11inda2  2112  moimv  2161  euim  2163  alral  2563  r19.12  2618  r19.27av  2643  r19.37  2651  eqvinc  2832  rr19.3v  2846  class2seteq  4073  dvdemo2  4105  dfwe2  4464  ordunisuc2  4526  tfindsg  4542  findsg  4574  asymref2  4967  sorpssuni  6138  sorpssint  6139  iotanul  6158  smo11  6267  omex  7228  r111  7331  kmlem12  7671  fin1a2lem10  7919  domtriomlem  7952  ltlen  8802  squeeze0  9539  elnnnn0b  9887  iccneg  10635  algcvgblem  12621  prmirred  16280  cxpcn2  19918  bpos1  20354  2bornot2b  20667  stcltr2i  22685  mdsl1i  22731  hbimtg  23331  idinside  23881  tb-ax2  23992  wl-jarri  24075  inttarcar  25067  a1i4  25367  prtlem1  25873  ax4567to4  26768  ax4567to5  26769  ax4567to6  26770  ax4567to7  26771  stoweidlem4  26887  pm2.43bgbi  27069  pm2.43cbi  27070  hbimpg  27110  hbimpgVD  27467  a9e2ndeqVD  27472  a9e2ndeqALT  27495  bnj1533  27670  bnj1176  27821  ax11dgenK  27928  ax12o10lem7K  27946  ax12o10lem7X  27947  ax12o10lem11K  27954  ax12o10lem11X  27955  a16gALTX  28002  a12study11  28042  a12study11n  28043  ax9lem9  28052  ax9lem10  28053  atpsubN  28846
  Copyright terms: Public domain W3C validator