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  3801  domtriomlem  10364  nn01to3  12891  xnn0lenn0nn0  13197  injresinjlem  13745  expnngt1  14203  reusq0  15427  dfgcd2  16515  lcmf  16602  prmgaplem5  17026  prmgaplem6  17027  cshwshashlem2  17067  mamufacex  22361  mavmulsolcl  22516  lgsqrmodndvds  27316  2sqreultlem  27410  2sqreunnltlem  27413  uspgrn2crct  29876  2pthon3v  30011  frgrreg  30464  ormkglobd  47305  icceuelpart  47896  prmdvdsfmtnof1lem2  48048  lighneallem4  48073  evenprm2  48190  suppmptcfin  48852  linc1  48901