MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  ax-1 Structured version   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  11  id  20  id1  21  a1d  23  a1dd  44  jarr  93  pm2.86i  94  pm2.86d  95  pm2.51  147  dfbi1gb  186  pm5.1im  230  biimt  326  pm5.4  352  pm4.8  355  olc  374  simpl  444  pm4.45im  546  pm2.64  765  pm2.74  820  pm2.82  826  oibabs  852  pm5.14  857  biort  867  dedlem0a  919  meredith  1413  tbw-bijust  1472  tbw-negdf  1473  tbw-ax2  1475  merco1  1487  ax12b  1701  ax11dgen  1737  19.38  1812  nfimdOLD  1828  hbimdOLD  1835  hbimOLD  1837  a16gOLD  2049  stdpc4  2087  sbi2  2120  ax11v  2171  ax11  2231  ax46to4  2239  ax467to4  2246  ax11f  2268  ax11eq  2269  ax11el  2270  ax11indi  2272  ax11indalem  2273  ax11inda2ALT  2274  ax11inda2  2275  morimv  2328  euim  2330  alral  2756  r19.12  2811  r19.27av  2836  r19.37  2849  eqvinc  3055  rr19.3v  3069  class2seteq  4360  dvdemo2  4392  dfwe2  4754  ordunisuc2  4816  tfindsg  4832  findsg  4864  asymref2  5243  iotanul  5425  sorpssuni  6523  sorpssint  6524  smo11  6618  omex  7590  r111  7693  kmlem12  8033  fin1a2lem10  8281  domtriomlem  8314  ltlen  9167  squeeze0  9905  elnnnn0b  10256  iccneg  11010  hash2prde  11680  algcvgblem  13060  prmirred  16767  cxpcn2  20622  bpos1  21059  usgra2edg  21394  nbgra0nb  21433  nbcusgra  21464  wlkdvspthlem  21599  usgrcyclnl2  21620  4cycl4dv  21646  2bornot2b  21750  stcltr2i  23770  mdsl1i  23816  eqvincg  23953  prsiga  24506  rpdmgm  24801  hbimtg  25426  idinside  26010  tb-ax2  26121  wl-jarri  26204  a1i4  26290  prtlem1  26681  ax4567to4  27570  ax4567to5  27571  ax4567to6  27572  ax4567to7  27573  cshwssizelem1a  28242  cshwssizelem3  28245  cshwssizelem4a  28246  frgra3vlem2  28328  frgranbnb  28347  frgrancvvdeqlem2  28357  pm2.43bgbi  28537  pm2.43cbi  28538  hbimpg  28578  hbimpgVD  28953  a9e2ndeqVD  28958  a9e2ndeqALT  28980  bnj1533  29160  bnj1176  29311  a16gNEW7  29483  stdpc4NEW7  29492  sbi2NEW7  29501  ax11vNEW7  29532  atpsubN  30487
  Copyright terms: Public domain W3C validator