Theorem 2a1 29

Description: A double form of ax-1 6. Its associated inference is 2a1i 12. Its associated deduction is 2a1d 27. (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 23	. 2 ⊢ (𝜑 → 𝜑)
2	1	2a1d 27	1 ⊢ (𝜑 → (𝜓 → (𝜒 → 𝜑)))

This proof depends on syntax axioms:   → wi 4

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7

This theorem is used by:  sbcg  3818  domtriomlem  10437  nn01to3  12976  xnn0lenn0nn0  13282  injresinjlem  13831  expnngt1  14290  reusq0  15535  dfgcd2  16621  lcmf  16708  prmgaplem5  17132  prmgaplem6  17133  cshwshashlem2  17173  mamufacex  22582  mavmulsolcl  22737  lgsqrmodndvds  27546  2sqreultlem  27640  2sqreunnltlem  27643  uspgrn2crct  30186  2pthon3v  30321  frgrreg  30774  ormkglobd  47624  icceuelpart  48218  prmdvdsfmtnof1lem2  48370  lighneallem4  48395  evenprm2  48512  suppmptcfin  49189  linc1  49238