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  3883  domtriomlem  10511  nn01to3  13006  xnn0lenn0nn0  13307  injresinjlem  13837  expnngt1  14290  reusq0  15511  dfgcd2  16593  lcmf  16680  prmgaplem5  17102  prmgaplem6  17103  cshwshashlem2  17144  mamufacex  22421  mavmulsolcl  22578  lgsqrmodndvds  27415  2sqreultlem  27509  2sqreunnltlem  27512  uspgrn2crct  29841  2pthon3v  29976  frgrreg  30426  icceuelpart  47310  prmdvdsfmtnof1lem2  47459  lighneallem4  47484  evenprm2  47588  suppmptcfin  48104  linc1  48154