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  3829  domtriomlem  10402  nn01to3  12907  xnn0lenn0nn0  13212  injresinjlem  13755  expnngt1  14213  reusq0  15438  dfgcd2  16523  lcmf  16610  prmgaplem5  17033  prmgaplem6  17034  cshwshashlem2  17074  mamufacex  22290  mavmulsolcl  22445  lgsqrmodndvds  27271  2sqreultlem  27365  2sqreunnltlem  27368  uspgrn2crct  29745  2pthon3v  29880  frgrreg  30330  ormkglobd  46880  icceuelpart  47441  prmdvdsfmtnof1lem2  47590  lighneallem4  47615  evenprm2  47719  suppmptcfin  48368  linc1  48418