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  1708  hbimd  1733  hbim  1737  nfimd  1773  a16g  1898  stdpc4  1977  sbi2  2017  ax11v  2049  ax11  2107  ax46to4  2115  ax467to4  2122  ax11f  2144  ax11eq  2145  ax11el  2146  ax11indi  2148  ax11indalem  2149  ax11inda2ALT  2150  ax11inda2  2151  morimv  2204  euim  2206  alral  2614  r19.12  2669  r19.27av  2694  r19.37  2702  eqvinc  2908  rr19.3v  2922  class2seteq  4195  dvdemo2  4227  dfwe2  4589  ordunisuc2  4651  tfindsg  4667  findsg  4699  asymref2  5076  iotanul  5250  sorpssuni  6302  sorpssint  6303  smo11  6397  omex  7360  r111  7463  kmlem12  7803  fin1a2lem10  8051  domtriomlem  8084  ltlen  8938  squeeze0  9675  elnnnn0b  10024  iccneg  10773  algcvgblem  12763  prmirred  16464  cxpcn2  20102  bpos1  20538  2bornot2b  20853  stcltr2i  22871  mdsl1i  22917  eqvincg  23146  prsiga  23507  hbimtg  24234  idinside  24779  tb-ax2  24890  wl-jarri  24973  inttarcar  26004  a1i4  26304  prtlem1  26810  ax4567to4  27705  ax4567to5  27706  ax4567to6  27707  ax4567to7  27708  stoweidlem4  27856  aibnbna  27977  nbgra0nb  28278  nbcusgra  28298  wlkdvspthlem  28365  usgrcyclnl2  28387  4cycl4dv  28413  frgra3vlem2  28425  pm2.43bgbi  28578  pm2.43cbi  28579  hbimpg  28619  hbimpgVD  28996  a9e2ndeqVD  29001  a9e2ndeqALT  29024  bnj1533  29200  bnj1176  29351  a16gNEW7  29521  stdpc4NEW7  29530  sbi2NEW7  29539  ax11vNEW7  29567  a12study11  29760  a12study11n  29761  ax9lem9  29770  ax9lem10  29771  atpsubN  30564
  Copyright terms: Public domain W3C validator