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  3814  domtriomlem  10333  nn01to3  12839  xnn0lenn0nn0  13144  injresinjlem  13690  expnngt1  14148  reusq0  15372  dfgcd2  16457  lcmf  16544  prmgaplem5  16967  prmgaplem6  16968  cshwshashlem2  17008  mamufacex  22312  mavmulsolcl  22467  lgsqrmodndvds  27292  2sqreultlem  27386  2sqreunnltlem  27389  uspgrn2crct  29787  2pthon3v  29922  frgrreg  30372  ormkglobd  46919  icceuelpart  47473  prmdvdsfmtnof1lem2  47622  lighneallem4  47647  evenprm2  47751  suppmptcfin  48413  linc1  48463