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  3817  domtriomlem  10355  nn01to3  12860  xnn0lenn0nn0  13165  injresinjlem  13708  expnngt1  14166  reusq0  15390  dfgcd2  16475  lcmf  16562  prmgaplem5  16985  prmgaplem6  16986  cshwshashlem2  17026  mamufacex  22299  mavmulsolcl  22454  lgsqrmodndvds  27280  2sqreultlem  27374  2sqreunnltlem  27377  uspgrn2crct  29771  2pthon3v  29906  frgrreg  30356  ormkglobd  46860  icceuelpart  47424  prmdvdsfmtnof1lem2  47573  lighneallem4  47598  evenprm2  47702  suppmptcfin  48364  linc1  48414