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

Axiom ax-1 5
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 4 . 2  wff  ( ps 
->  ph )
41, 3wi 4 1  wff  ( ph  ->  ( ps  ->  ph )
)
Colors of variables: wff set class
This axiom is referenced by:  a1i  10  id  19  id1  20  a1d  22  a1dd  42  jarr  91  pm2.86i  92  pm2.86d  93  pm2.51  145  dfbi1gb  185  pm5.1im  229  biimt  325  pm5.4  351  pm4.8  354  olc  373  simpl  443  pm4.45im  545  pm2.64  764  pm2.74  819  pm2.82  825  oibabs  851  pm5.14  856  biort  866  dedlem0a  918  meredith  1394  tbw-bijust  1453  tbw-negdf  1454  tbw-ax2  1456  merco1  1468  ax11dgen  1696  hbimd  1721  hbim  1725  nfimd  1761  a16g  1885  stdpc4  1964  sbi2  2004  ax11v  2036  ax11  2094  ax46to4  2102  ax467to4  2109  ax11f  2131  ax11eq  2132  ax11el  2133  ax11indi  2135  ax11indalem  2136  ax11inda2ALT  2137  ax11inda2  2138  morimv  2191  euim  2193  alral  2601  r19.12  2656  r19.27av  2681  r19.37  2689  eqvinc  2895  rr19.3v  2909  class2seteq  4179  dvdemo2  4211  dfwe2  4573  ordunisuc2  4635  tfindsg  4651  findsg  4683  asymref2  5060  iotanul  5234  sorpssuni  6286  sorpssint  6287  smo11  6381  omex  7344  r111  7447  kmlem12  7787  fin1a2lem10  8035  domtriomlem  8068  ltlen  8922  squeeze0  9659  elnnnn0b  10008  iccneg  10757  algcvgblem  12747  prmirred  16448  cxpcn2  20086  bpos1  20522  2bornot2b  20837  stcltr2i  22855  mdsl1i  22901  eqvincg  23130  prsiga  23492  hbimtg  24163  idinside  24707  tb-ax2  24818  wl-jarri  24901  inttarcar  25901  a1i4  26201  prtlem1  26707  ax4567to4  27602  ax4567to5  27603  ax4567to6  27604  ax4567to7  27605  stoweidlem4  27753  aibnbna  27874  nbgra0nb  28144  nbcusgra  28159  frgra3vlem2  28179  pm2.43bgbi  28279  pm2.43cbi  28280  hbimpg  28320  hbimpgVD  28680  a9e2ndeqVD  28685  a9e2ndeqALT  28708  bnj1533  28884  bnj1176  29035  a12study11  29138  a12study11n  29139  ax9lem9  29148  ax9lem10  29149  atpsubN  29942
  Copyright terms: Public domain W3C validator