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  9264  nn01to3  11781  xnn0lenn0nn0  12075  injresinjlem  12588  dfgcd2  15263  lcmf  15346  cshwshashlem2  15803  mamufacex  20195  mavmulsolcl  20357  lgsqrmodndvds  25078  uspgrn2crct  26700  2pthon3v  26839  frgrreg  27252  icceuelpart  41372  prmdvdsfmtnof1lem2  41497  lighneallem4  41527  evenprm2  41623  suppmptcfin  42160  linc1  42214