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  214  pm5.1im  263  biimt  360  pm4.8  392  pm4.45im  827  pm5.31r  831  jao1i  858  olc  868  oibabs  953  pm2.74  976  tarski-bernays-ax2  1640  meredith  1641  tbw-bijust  1698  tbw-negdf  1699  tbw-ax2  1701  merco1  1713  nftht  1792  ala1  1813  exa1  1838  ax13b  2031  sbi2  2302  ax12vALT  2473  moabs  2542  moa1  2550  r19.35  3095  r19.35OLD  3096  r19.21v  3165  r19.37  3245  eqvincg  3627  rr19.3v  3646  class2seteq  3687  ralidmw  4483  ralidm  4487  dvdemo2  5344  iunopeqop  5496  po2ne  5577  asymref2  6106  elfv2ex  6921  elovmpt3imp  7662  sorpssuni  7724  dfwe2  7766  ordunisuc2  7837  xpord3ind  8153  smo11  8376  omex  9655  r111  9787  kmlem12  10174  squeeze0  12143  nn0ge2m1nn  12569  nn0lt10b  12653  iccneg  13487  hashfzp1  14447  hash2prde  14486  hash2pwpr  14492  hashge2el2dif  14496  hash3tpde  14509  relexprel  15056  algcvgblem  16594  prm23ge5  16833  cshwshashlem1  17113  dfgrp2e  18944  gsmtrcl  19495  nzerooringczr  21439  symgmatr01lem  22589  cxpcn2  26706  logbgcd1irr  26754  rpdmgm  26985  bpos1  27244  2lgs  27368  2sqnn0  27399  umgrislfupgrlem  29047  uhgr2edg  29133  nbusgrvtxm1  29304  uvtx01vtx  29322  g0wlk0  29578  wlkonl1iedg  29591  wlkreslem  29595  crctcshwlkn0lem5  29742  0enwwlksnge1  29792  clwwlknonex2lem2  30035  frgr3vlem2  30201  frgrnbnb  30220  frgrregord013  30322  frgrogt3nreg  30324  2bornot2b  30391  stcltr2i  32202  mdsl1i  32248  prsiga  34108  logdivsqrle  34628  bnj1533  34829  bnj1176  34982  jath  35688  idinside  36048  tb-ax2  36348  bj-a1k  36508  bj-peircestab  36517  bj-currypeirce  36521  bj-andnotim  36552  bj-ssbeq  36617  bj-eqs  36639  bj-nnftht  36705  curryset  36910  currysetlem3  36913  wl-moae  37480  tsim3  38102  mpobi123f  38132  mptbi12f  38136  ac6s6  38142  ax12fromc15  38869  axc5c7toc5  38876  axc5c711toc5  38883  ax12f  38904  ax12eq  38905  ax12el  38906  ax12indi  38908  ax12indalem  38909  ax12inda2ALT  38910  ax12inda2  38911  atpsubN  39718  ifpim23g  43466  rp-fakeimass  43483  inintabss  43549  ntrneiiso  44062  spALT  44172  axc5c4c711toc5  44374  axc5c4c711toc4  44375  axc5c4c711toc7  44376  axc5c4c711to11  44377  pm2.43bgbi  44490  pm2.43cbi  44491  hbimpg  44527  hbimpgVD  44876  ax6e2ndeqVD  44881  ax6e2ndeqALT  44903  dfbi1ALTa  44912  simprimi  44913  ralimralim  45053  confun  46916  confun5  46920  adh-jarrsc  46977  adh-minim  46978  adh-minimp  46990  f1cof1b  47054  iccpartnel  47400  fmtno4prmfac193  47535  prminf2  47550  zeo2ALTV  47633  fpprbasnn  47691  sbgoldbaltlem1  47741  elclnbgrelnbgr  47787  islinindfis  48373  lindslinindsimp2lem5  48386  zlmodzxznm  48421