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  3855  domtriomlem  10433  nn01to3  12921  xnn0lenn0nn0  13220  injresinjlem  13748  expnngt1  14200  reusq0  15405  dfgcd2  16484  lcmf  16566  prmgaplem5  16984  prmgaplem6  16985  cshwshashlem2  17026  mamufacex  21873  mavmulsolcl  22035  lgsqrmodndvds  26836  2sqreultlem  26930  2sqreunnltlem  26933  uspgrn2crct  29042  2pthon3v  29177  frgrreg  29627  icceuelpart  46039  prmdvdsfmtnof1lem2  46188  lighneallem4  46213  evenprm2  46317  suppmptcfin  46957  linc1  47008