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  9147  nn01to3  11657  injresinjlem  12450  dfgcd2  15101  lcmf  15184  cshwshashlem2  15641  mamufacex  20014  mavmulsolcl  20176  lgsqrmodndvds  24878  wlkdvspthlem  26137  clwwlkgt0  26299  frgrareg  26644  icceuelpart  39974  prmdvdsfmtnof1lem2  40035  lighneallem4  40065  evenprm2  40161  uspgrn2crct  41011  2pthon3v-av  41150  av-frgrareg  41548  suppmptcfin  41954  linc1  42008