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  3795  domtriomlem  10356  nn01to3  12883  xnn0lenn0nn0  13189  injresinjlem  13737  expnngt1  14195  reusq0  15419  dfgcd2  16507  lcmf  16594  prmgaplem5  17018  prmgaplem6  17019  cshwshashlem2  17059  mamufacex  22380  mavmulsolcl  22535  lgsqrmodndvds  27335  2sqreultlem  27429  2sqreunnltlem  27432  uspgrn2crct  29895  2pthon3v  30030  frgrreg  30483  ormkglobd  47328  icceuelpart  47919  prmdvdsfmtnof1lem2  48071  lighneallem4  48096  evenprm2  48213  suppmptcfin  48875  linc1  48924