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  3843  domtriomlem  10461  nn01to3  12962  xnn0lenn0nn0  13266  injresinjlem  13808  expnngt1  14264  reusq0  15486  dfgcd2  16570  lcmf  16657  prmgaplem5  17080  prmgaplem6  17081  cshwshashlem2  17121  mamufacex  22339  mavmulsolcl  22494  lgsqrmodndvds  27321  2sqreultlem  27415  2sqreunnltlem  27418  uspgrn2crct  29795  2pthon3v  29930  frgrreg  30380  ormkglobd  46871  icceuelpart  47417  prmdvdsfmtnof1lem2  47566  lighneallem4  47591  evenprm2  47695  suppmptcfin  48318  linc1  48368