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  19954  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  pm2.43bgbi  26972  pm2.43cbi  26973  hbimpg  27013  hbimpgVD  27370  a9e2ndeqVD  27375  a9e2ndeqALT  27398  bnj1533  27573  bnj1176  27724  a12study11  27827  a12study11n  27828  ax9lem9  27837  ax9lem10  27838  atpsubN  28631
  Copyright terms: Public domain W3C validator