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  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  1410  tbw-bijust  1469  tbw-negdf  1470  tbw-ax2  1472  merco1  1484  ax12b  1697  ax11dgen  1733  19.38  1808  nfimdOLD  1824  hbimdOLD  1831  hbimOLD  1833  a16gOLD  2013  stdpc4  2073  sbi2  2113  ax11v  2145  ax11  2205  ax46to4  2213  ax467to4  2220  ax11f  2242  ax11eq  2243  ax11el  2244  ax11indi  2246  ax11indalem  2247  ax11inda2ALT  2248  ax11inda2  2249  morimv  2302  euim  2304  alral  2724  r19.12  2779  r19.27av  2804  r19.37  2817  eqvinc  3023  rr19.3v  3037  class2seteq  4328  dvdemo2  4360  dfwe2  4721  ordunisuc2  4783  tfindsg  4799  findsg  4831  asymref2  5210  iotanul  5392  sorpssuni  6490  sorpssint  6491  smo11  6585  omex  7554  r111  7657  kmlem12  7997  fin1a2lem10  8245  domtriomlem  8278  ltlen  9131  squeeze0  9869  elnnnn0b  10220  iccneg  10974  hash2prde  11643  algcvgblem  13023  prmirred  16730  cxpcn2  20583  bpos1  21020  usgra2edg  21355  nbgra0nb  21394  nbcusgra  21425  wlkdvspthlem  21560  usgrcyclnl2  21581  4cycl4dv  21607  2bornot2b  21711  stcltr2i  23731  mdsl1i  23777  eqvincg  23914  prsiga  24467  rpdmgm  24762  hbimtg  25377  idinside  25922  tb-ax2  26033  wl-jarri  26116  a1i4  26189  prtlem1  26580  ax4567to4  27470  ax4567to5  27471  ax4567to6  27472  ax4567to7  27473  frgra3vlem2  28105  frgranbnb  28124  frgrancvvdeqlem2  28134  pm2.43bgbi  28311  pm2.43cbi  28312  hbimpg  28352  hbimpgVD  28725  a9e2ndeqVD  28730  a9e2ndeqALT  28753  bnj1533  28929  bnj1176  29080  a16gNEW7  29250  stdpc4NEW7  29259  sbi2NEW7  29268  ax11vNEW7  29296  atpsubN  30235
  Copyright terms: Public domain W3C validator