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  3810  domtriomlem  10524  nn01to3  13072  xnn0lenn0nn0  13379  injresinjlem  13929  expnngt1  14389  reusq0  15638  dfgcd2  16725  lcmf  16814  prmgaplem5  17239  prmgaplem6  17240  cshwshashlem2  17280  mamufacex  22717  mavmulsolcl  22872  lgsqrmodndvds  27686  2sqreultlem  27780  2sqreunnltlem  27783  uspgrn2crct  30403  2pthon3v  30538  frgrreg  31001  ormkglobd  47981  icceuelpart  48612  prmdvdsfmtnof1lem2  48764  lighneallem4  48789  evenprm2  48906  suppmptcfin  49582  linc1  49631