Theorem 2a1 28

Description: A double form of ax-1 6. Its associated inference is 2a1i 12. Its associated deduction is 2a1d 26. (Contributed by BJ, 10-Aug-2020.) (Proof shortened by Wolf Lammen, 1-Sep-2020.)

Assertion

Ref	Expression
2a1	⊢ (𝜑 → (𝜓 → (𝜒 → 𝜑)))

Proof of Theorem 2a1

Step	Hyp	Ref	Expression
1		id 22	. 2 ⊢ (𝜑 → 𝜑)
2	1	2a1d 26	1 ⊢ (𝜑 → (𝜓 → (𝜒 → 𝜑)))

Syntax hints:   → wi 4

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7

This theorem is referenced by:  sbcg  3802  domtriomlem  10355  nn01to3  12882  xnn0lenn0nn0  13188  injresinjlem  13736  expnngt1  14194  reusq0  15418  dfgcd2  16506  lcmf  16593  prmgaplem5  17017  prmgaplem6  17018  cshwshashlem2  17058  mamufacex  22371  mavmulsolcl  22526  lgsqrmodndvds  27330  2sqreultlem  27424  2sqreunnltlem  27427  uspgrn2crct  29891  2pthon3v  30026  frgrreg  30479  ormkglobd  47321  icceuelpart  47908  prmdvdsfmtnof1lem2  48060  lighneallem4  48085  evenprm2  48202  suppmptcfin  48864  linc1  48913