MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  2a1 Structured version   Visualization version   GIF version

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
StepHypRef Expression
1 id 22 . 2 (𝜑𝜑)
212a1d 26 1 (𝜑 → (𝜓 → (𝜒𝜑)))
Colors of variables: wff setvar class
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  3855  domtriomlem  10433  nn01to3  12921  xnn0lenn0nn0  13220  injresinjlem  13748  expnngt1  14200  reusq0  15405  dfgcd2  16484  lcmf  16566  prmgaplem5  16984  prmgaplem6  16985  cshwshashlem2  17026  mamufacex  21873  mavmulsolcl  22035  lgsqrmodndvds  26836  2sqreultlem  26930  2sqreunnltlem  26933  uspgrn2crct  29042  2pthon3v  29177  frgrreg  29627  icceuelpart  46039  prmdvdsfmtnof1lem2  46188  lighneallem4  46213  evenprm2  46317  suppmptcfin  46957  linc1  47008
  Copyright terms: Public domain W3C validator