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:  domtriomlem  9208  nn01to3  11725  xnn0lenn0nn0  12018  injresinjlem  12528  dfgcd2  15187  lcmf  15270  cshwshashlem2  15727  mamufacex  20114  mavmulsolcl  20276  lgsqrmodndvds  24978  uspgrn2crct  26569  2pthon3v  26708  frgrreg  27106  icceuelpart  40670  prmdvdsfmtnof1lem2  40796  lighneallem4  40826  evenprm2  40922  suppmptcfin  41448  linc1  41502
  Copyright terms: Public domain W3C validator