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  3813  domtriomlem  10352  nn01to3  12854  xnn0lenn0nn0  13160  injresinjlem  13706  expnngt1  14164  reusq0  15388  dfgcd2  16473  lcmf  16560  prmgaplem5  16983  prmgaplem6  16984  cshwshashlem2  17024  mamufacex  22340  mavmulsolcl  22495  lgsqrmodndvds  27320  2sqreultlem  27414  2sqreunnltlem  27417  uspgrn2crct  29881  2pthon3v  30016  frgrreg  30469  ormkglobd  47119  icceuelpart  47682  prmdvdsfmtnof1lem2  47831  lighneallem4  47856  evenprm2  47960  suppmptcfin  48622  linc1  48671