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  3802  domtriomlem  10362  nn01to3  12889  xnn0lenn0nn0  13195  injresinjlem  13743  expnngt1  14201  reusq0  15425  dfgcd2  16513  lcmf  16600  prmgaplem5  17024  prmgaplem6  17025  cshwshashlem2  17065  mamufacex  22386  mavmulsolcl  22541  lgsqrmodndvds  27341  2sqreultlem  27435  2sqreunnltlem  27438  uspgrn2crct  29901  2pthon3v  30036  frgrreg  30489  ormkglobd  47327  icceuelpart  47918  prmdvdsfmtnof1lem2  48070  lighneallem4  48095  evenprm2  48212  suppmptcfin  48874  linc1  48923