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  3815  domtriomlem  10364  nn01to3  12866  xnn0lenn0nn0  13172  injresinjlem  13718  expnngt1  14176  reusq0  15400  dfgcd2  16485  lcmf  16572  prmgaplem5  16995  prmgaplem6  16996  cshwshashlem2  17036  mamufacex  22352  mavmulsolcl  22507  lgsqrmodndvds  27332  2sqreultlem  27426  2sqreunnltlem  27429  uspgrn2crct  29893  2pthon3v  30028  frgrreg  30481  ormkglobd  47230  icceuelpart  47793  prmdvdsfmtnof1lem2  47942  lighneallem4  47967  evenprm2  48071  suppmptcfin  48733  linc1  48782