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." (Contributed by NM, 5-Aug-1993.)

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  10  id  19  idALT  20  a1d  22  a1dd  42  jarr  91  pm2.86i  92  pm2.86d  93  pm2.51  145  dfbi1gb  185  pm5.1im  229  biimt  325  pm5.4  351  pm4.8  354  olc  373  simpl  443  pm4.45im  545  pm2.64  764  pm2.74  819  pm2.82  825  oibabs  851  pm5.14  856  biort  866  dedlem0a  918  meredith  1404  tbw-bijust  1463  tbw-negdf  1464  tbw-ax2  1466  merco1  1478  ax11dgen  1722  19.38  1794  nfimdOLD  1809  hbimdOLD  1816  hbimOLD  1818  a16g  1945  stdpc4  2024  sbi2  2064  ax11v  2096  ax11  2155  ax46to4  2163  ax467to4  2170  ax11f  2192  ax11eq  2193  ax11el  2194  ax11indi  2196  ax11indalem  2197  ax11inda2ALT  2198  ax11inda2  2199  morimv  2252  euim  2254  alral  2673  r19.12  2728  r19.27av  2753  r19.37  2761  eqvinc  2967  rr19.3v  2981  pwadjoin  4120  iotanul  4355