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  3811  domtriomlem  10444  nn01to3  12990  xnn0lenn0nn0  13297  injresinjlem  13846  expnngt1  14305  reusq0  15552  dfgcd2  16636  lcmf  16723  prmgaplem5  17147  prmgaplem6  17148  cshwshashlem2  17188  mamufacex  22618  mavmulsolcl  22773  lgsqrmodndvds  27589  2sqreultlem  27683  2sqreunnltlem  27686  uspgrn2crct  30276  2pthon3v  30411  frgrreg  30874  ormkglobd  47705  icceuelpart  48336  prmdvdsfmtnof1lem2  48488  lighneallem4  48513  evenprm2  48630  suppmptcfin  49306  linc1  49355