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  3817  domtriomlem  10427  nn01to3  12966  xnn0lenn0nn0  13272  injresinjlem  13821  expnngt1  14279  reusq0  15518  dfgcd2  16605  lcmf  16692  prmgaplem5  17116  prmgaplem6  17117  cshwshashlem2  17157  mamufacex  22534  mavmulsolcl  22689  lgsqrmodndvds  27498  2sqreultlem  27592  2sqreunnltlem  27595  uspgrn2crct  30138  2pthon3v  30273  frgrreg  30726  ormkglobd  47574  icceuelpart  48168  prmdvdsfmtnof1lem2  48320  lighneallem4  48345  evenprm2  48462  suppmptcfin  49139  linc1  49188