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  3810  domtriomlem  10342  nn01to3  12843  xnn0lenn0nn0  13148  injresinjlem  13694  expnngt1  14152  reusq0  15376  dfgcd2  16461  lcmf  16548  prmgaplem5  16971  prmgaplem6  16972  cshwshashlem2  17012  mamufacex  22314  mavmulsolcl  22469  lgsqrmodndvds  27294  2sqreultlem  27388  2sqreunnltlem  27391  uspgrn2crct  29790  2pthon3v  29925  frgrreg  30378  ormkglobd  47000  icceuelpart  47563  prmdvdsfmtnof1lem2  47712  lighneallem4  47737  evenprm2  47841  suppmptcfin  48503  linc1  48553