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:  domtriomlem  9866  nn01to3  12344  xnn0lenn0nn0  12641  injresinjlem  13160  expnngt1  13605  reusq0  14824  dfgcd2  15896  lcmf  15979  prmgaplem5  16393  prmgaplem6  16394  cshwshashlem2  16432  mamufacex  21002  mavmulsolcl  21162  lgsqrmodndvds  25931  2sqreultlem  26025  2sqreunnltlem  26028  uspgrn2crct  27588  2pthon3v  27724  frgrreg  28175  icceuelpart  43603  prmdvdsfmtnof1lem2  43754  lighneallem4  43782  evenprm2  43886  suppmptcfin  44434  linc1  44487