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  3857  domtriomlem  10437  nn01to3  12925  xnn0lenn0nn0  13224  injresinjlem  13752  expnngt1  14204  reusq0  15409  dfgcd2  16488  lcmf  16570  prmgaplem5  16988  prmgaplem6  16989  cshwshashlem2  17030  mamufacex  21891  mavmulsolcl  22053  lgsqrmodndvds  26856  2sqreultlem  26950  2sqreunnltlem  26953  uspgrn2crct  29062  2pthon3v  29197  frgrreg  29647  icceuelpart  46104  prmdvdsfmtnof1lem2  46253  lighneallem4  46278  evenprm2  46382  suppmptcfin  47055  linc1  47106