Theorem 2a1 29

Description: A double form of ax-1 6. Its associated inference is 2a1i 12. Its associated deduction is 2a1d 27. (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 23	. 2 ⊢ (𝜑 → 𝜑)
2	1	2a1d 27	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  3819  domtriomlem  10414  nn01to3  12953  xnn0lenn0nn0  13259  injresinjlem  13807  expnngt1  14265  reusq0  15504  dfgcd2  16592  lcmf  16679  prmgaplem5  17103  prmgaplem6  17104  cshwshashlem2  17144  mamufacex  22510  mavmulsolcl  22665  lgsqrmodndvds  27471  2sqreultlem  27565  2sqreunnltlem  27568  uspgrn2crct  30062  2pthon3v  30197  frgrreg  30650  ormkglobd  47450  icceuelpart  48041  prmdvdsfmtnof1lem2  48193  lighneallem4  48218  evenprm2  48335  suppmptcfin  49008  linc1  49057