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  3795  domtriomlem  10198  nn01to3  12681  xnn0lenn0nn0  12979  injresinjlem  13507  expnngt1  13956  reusq0  15174  dfgcd2  16254  lcmf  16338  prmgaplem5  16756  prmgaplem6  16757  cshwshashlem2  16798  mamufacex  21538  mavmulsolcl  21700  lgsqrmodndvds  26501  2sqreultlem  26595  2sqreunnltlem  26598  uspgrn2crct  28173  2pthon3v  28308  frgrreg  28758  icceuelpart  44888  prmdvdsfmtnof1lem2  45037  lighneallem4  45062  evenprm2  45166  suppmptcfin  45715  linc1  45766