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:  domtriomlem  9579  nn01to3  12064  xnn0lenn0nn0  12363  injresinjlem  12883  expnngt1  13322  dfgcd2  15636  lcmf  15719  cshwshashlem2  16169  mamufacex  20562  mavmulsolcl  20725  lgsqrmodndvds  25491  uspgrn2crct  27107  2pthon3v  27272  frgrreg  27809  icceuelpart  42260  prmdvdsfmtnof1lem2  42327  lighneallem4  42357  evenprm2  42453  suppmptcfin  43007  linc1  43061