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  3863  domtriomlem  10482  nn01to3  12983  xnn0lenn0nn0  13287  injresinjlem  13826  expnngt1  14280  reusq0  15501  dfgcd2  16583  lcmf  16670  prmgaplem5  17093  prmgaplem6  17094  cshwshashlem2  17134  mamufacex  22400  mavmulsolcl  22557  lgsqrmodndvds  27397  2sqreultlem  27491  2sqreunnltlem  27494  uspgrn2crct  29828  2pthon3v  29963  frgrreg  30413  ormkglobd  46890  icceuelpart  47423  prmdvdsfmtnof1lem2  47572  lighneallem4  47597  evenprm2  47701  suppmptcfin  48292  linc1  48342