Axiom ax-1 6

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 𝜑 and 𝜓 to the assertion of 𝜑 simply". It is Proposition 1 of [Frege1879] p. 26, its first axiom. (Contributed by NM, 30-Sep-1992.)

Assertion

Ref	Expression
ax-1	⊢ (𝜑 → (𝜓 → 𝜑))

Detailed syntax breakdown of Axiom ax-1

Step	Hyp	Ref	Expression
1		wph	. 2 wff 𝜑
2		wps	. . 3 wff 𝜓
3	2, 1	wi 4	. 2 wff (𝜓 → 𝜑)
4	1, 3	wi 4	1 wff (𝜑 → (𝜓 → 𝜑))

This axiom is referenced by:  a1i  11  id  22  idALT  23  a1d  25  a1dd  50  a1ddd  80  jarr  106  jarri  107  pm2.86d  108  conax1  170  dfbi1ALT  216  pm5.1im  265  biimt  362  pm4.8  394  pm4.45im  834  pm5.31r  838  jao1i  865  olc  875  oibabs  960  pm2.74  983  tarski-bernays-ax2  1648  meredith  1649  tbw-bijust  1706  tbw-negdf  1707  tbw-ax2  1709  merco1  1721  nftht  1800  ala1  1821  exa1  1846  ax13b  2040  sbrimvw  2103  sbi2  2315  ax12vALT  2479  moabs  2549  moa1  2557  r19.35  3099  r19.21v  3166  r19.37  3244  eqvincg  3587  rr19.3v  3606  class2seteq  3646  r19.3rzv  4433  ralidmw  4446  ralidm  4447  dvdemo2  5305  iunopeqop  5464  iunopeqopOLD  5465  po2ne  5544  asymref2  6073  elfv2ex  6873  elovmpt3imp  7616  sorpssuni  7678  dfwe2  7720  ordunisuc2  7787  xpord3ind  8098  smo11  8297  omex  9559  r111  9694  kmlem12  10079  squeeze0  12054  nn0ge2m1nn  12502  nn0lt10b  12586  iccneg  13420  hashfzp1  14388  hash2prde  14427  hash2pwpr  14433  hashge2el2dif  14437  hash3tpde  14450  relexprel  14996  algcvgblem  16541  prm23ge5  16781  cshwshashlem1  17061  dfgrp2e  18934  gsmtrcl  19485  nzerooringczr  21458  symgmatr01lem  22639  cxpcn2  26731  logbgcd1irr  26779  rpdmgm  27009  bpos1  27267  2lgs  27391  2sqnn0  27422  umgrislfupgrlem  29211  uhgr2edg  29297  nbusgrvtxm1  29468  uvtx01vtx  29486  g0wlk0  29739  wlkonl1iedg  29752  wlkreslem  29756  crctcshwlkn0lem5  29902  0enwwlksnge1  29952  clwwlknonex2lem2  30198  frgr3vlem2  30364  frgrnbnb  30383  frgrregord013  30485  frgrogt3nreg  30487  2bornot2b  30554  stcltr2i  32366  mdsl1i  32412  prsiga  34325  logdivsqrle  34844  bnj1533  35047  bnj1176  35200  axprALT2  35303  onvf1odlem1  35344  jath  35966  idinside  36325  tb-ax2  36625  bj-a1k  36863  bj-peircestab  36874  bj-currypeirce  36880  bj-andnotim  36912  bj-ssbeq  37006  bj-eqs  37029  bj-alnnf  37093  curryset  37312  currysetlem3  37315  wl-moae  37900  tsim3  38512  mpobi123f  38542  mptbi12f  38546  ac6s6  38552  ax12fromc15  39410  axc5c7toc5  39417  axc5c711toc5  39424  ax12f  39445  ax12eq  39446  ax12el  39447  ax12indi  39449  ax12indalem  39450  ax12inda2ALT  39451  ax12inda2  39452  atpsubN  40258  ifpim23g  43952  rp-fakeimass  43969  inintabss  44035  ntrneiiso  44548  spALT  44658  axc5c4c711toc5  44859  axc5c4c711toc4  44860  axc5c4c711toc7  44861  axc5c4c711to11  44862  pm2.43bgbi  44974  pm2.43cbi  44975  hbimpg  45011  hbimpgVD  45360  ax6e2ndeqVD  45365  ax6e2ndeqALT  45387  dfbi1ALTa  45396  simprimi  45397  ralimralim  45542  confun  47414  confun5  47418  adh-jarrsc  47475  adh-minim  47476  adh-minimp  47488  f1cof1b  47552  iccpartnel  47925  fmtno4prmfac193  48063  prminf2  48078  zeo2ALTV  48174  fpprbasnn  48232  sbgoldbaltlem1  48282  elclnbgrelnbgr  48328  pgnbgreunbgrlem2lem1  48617  pgnbgreunbgrlem2lem2  48618  pgnbgreunbgrlem2lem3  48619  islinindfis  48952  lindslinindsimp2lem5  48965  zlmodzxznm  49000