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  3791  domtriomlem  10129  nn01to3  12610  xnn0lenn0nn0  12908  injresinjlem  13435  expnngt1  13884  reusq0  15102  dfgcd2  16182  lcmf  16266  prmgaplem5  16684  prmgaplem6  16685  cshwshashlem2  16726  mamufacex  21448  mavmulsolcl  21608  lgsqrmodndvds  26406  2sqreultlem  26500  2sqreunnltlem  26503  uspgrn2crct  28074  2pthon3v  28209  frgrreg  28659  icceuelpart  44776  prmdvdsfmtnof1lem2  44925  lighneallem4  44950  evenprm2  45054  suppmptcfin  45603  linc1  45654