Theorem 2a1 29

Description: A double form of ax-1 6. Its associated inference is 2a1i 12. Its associated deduction is 2a1d 27. (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 23	. 2 ⊢ (𝜑 → 𝜑)
2	1	2a1d 27	1 ⊢ (𝜑 → (𝜓 → (𝜒 → 𝜑)))

This proof depends on syntax axioms:   → wi 4

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7

This theorem is used by:  sbcg  3814  domtriomlem  10559  nn01to3  13108  xnn0lenn0nn0  13415  injresinjlem  13965  expnngt1  14426  reusq0  15676  dfgcd2  16763  lcmf  16852  prmgaplem5  17277  prmgaplem6  17278  cshwshashlem2  17318  mamufacex  22766  mavmulsolcl  22921  lgsqrmodndvds  27737  2sqreultlem  27831  2sqreunnltlem  27834  uspgrn2crct  30454  2pthon3v  30589  frgrreg  31052  ormkglobd  48160  icceuelpart  48791  prmdvdsfmtnof1lem2  48943  lighneallem4  48968  evenprm2  49085  suppmptcfin  49819  linc1  49868