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:  sbcg  3814  domtriomlem  10392  nn01to3  12935  xnn0lenn0nn0  13241  injresinjlem  13789  expnngt1  14247  reusq0  15482  dfgcd2  16570  lcmf  16657  prmgaplem5  17081  prmgaplem6  17082  cshwshashlem2  17122  mamufacex  22443  mavmulsolcl  22598  lgsqrmodndvds  27404  2sqreultlem  27498  2sqreunnltlem  27501  uspgrn2crct  29964  2pthon3v  30099  frgrreg  30552  ormkglobd  47411  icceuelpart  48002  prmdvdsfmtnof1lem2  48154  lighneallem4  48179  evenprm2  48296  suppmptcfin  48958  linc1  49007