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  3826  domtriomlem  10395  nn01to3  12900  xnn0lenn0nn0  13205  injresinjlem  13748  expnngt1  14206  reusq0  15431  dfgcd2  16516  lcmf  16603  prmgaplem5  17026  prmgaplem6  17027  cshwshashlem2  17067  mamufacex  22283  mavmulsolcl  22438  lgsqrmodndvds  27264  2sqreultlem  27358  2sqreunnltlem  27361  uspgrn2crct  29738  2pthon3v  29873  frgrreg  30323  ormkglobd  46873  icceuelpart  47434  prmdvdsfmtnof1lem2  47583  lighneallem4  47608  evenprm2  47712  suppmptcfin  48361  linc1  48411