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  766  pm2.74  821  pm2.82  827  oibabs  853  pm5.14  858  biort  868  dedlem0a  920  meredith  1396  tbw-bijust  1455  tbw-negdf  1456  tbw-ax2  1458  merco1  1470  ax11f  1631  ax11dgen  1699  hbimd  1725  hbim  1729  nfimd  1765  a16gALT  1889  stdpc4  1971  sbi2  2005  ax11v  2038  ax11  2098  ax46to4  2106  ax467to4  2113  ax11eq  2135  ax11el  2136  ax11indi  2138  ax11indalem  2139  ax11inda2ALT  2140  ax11inda2  2141  morimv  2194  euim  2196  alral  2604  r19.12  2659  r19.27av  2684  r19.37  2692  eqvinc  2898  rr19.3v  2912  class2seteq  4180  dvdemo2  4212  dfwe2  4574  ordunisuc2  4636  tfindsg  4652  findsg  4684  asymref2  5061  sorpssuni  6249  sorpssint  6250  iotanul  6269  smo11  6378  omex  7341  r111  7444  kmlem12  7784  fin1a2lem10  8032  domtriomlem  8065  ltlen  8919  squeeze0  9656  elnnnn0b  10005  iccneg  10753  algcvgblem  12743  prmirred  16444  cxpcn2  20082  bpos1  20518  2bornot2b  20831  stcltr2i  22849  mdsl1i  22895  hbimtg  23566  idinside  24116  tb-ax2  24227  wl-jarri  24310  inttarcar  25302  a1i4  25602  prtlem1  26108  ax4567to4  27003  ax4567to5  27004  ax4567to6  27005  ax4567to7  27006  stoweidlem4  27154  aibnbna  27255  pm2.43bgbi  27552  pm2.43cbi  27553  hbimpg  27593  hbimpgVD  27950  a9e2ndeqVD  27955  a9e2ndeqALT  27978  bnj1533  28153  bnj1176  28304  a12study11  28407  a12study11n  28408  ax9lem9  28417  ax9lem10  28418  atpsubN  29211
  Copyright terms: Public domain W3C validator