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  10513  nn01to3  13061  xnn0lenn0nn0  13368  injresinjlem  13918  expnngt1  14378  reusq0  15625  dfgcd2  16712  lcmf  16801  prmgaplem5  17226  prmgaplem6  17227  cshwshashlem2  17267  mamufacex  22704  mavmulsolcl  22859  lgsqrmodndvds  27673  2sqreultlem  27767  2sqreunnltlem  27770  uspgrn2crct  30390  2pthon3v  30525  frgrreg  30988  ormkglobd  47856  icceuelpart  48487  prmdvdsfmtnof1lem2  48639  lighneallem4  48664  evenprm2  48781  suppmptcfin  49457  linc1  49506