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:  domtriomlem  9868  nn01to3  12346  xnn0lenn0nn0  12643  injresinjlem  13169  expnngt1  13615  reusq0  14831  dfgcd2  15901  lcmf  15984  prmgaplem5  16398  prmgaplem6  16399  cshwshashlem2  16439  mamufacex  21034  mavmulsolcl  21194  lgsqrmodndvds  25978  2sqreultlem  26072  2sqreunnltlem  26075  uspgrn2crct  27635  2pthon3v  27770  frgrreg  28220  icceuelpart  44037  prmdvdsfmtnof1lem2  44186  lighneallem4  44212  evenprm2  44316  suppmptcfin  44865  linc1  44916
 Copyright terms: Public domain W3C validator