Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > MPE Home > Th. List > 2a1 | Structured version Visualization version GIF version |
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.) |
Ref | Expression |
---|---|
2a1 | ⊢ (𝜑 → (𝜓 → (𝜒 → 𝜑))) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | id 22 | . 2 ⊢ (𝜑 → 𝜑) | |
2 | 1 | 2a1d 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 9866 nn01to3 12344 xnn0lenn0nn0 12641 injresinjlem 13160 expnngt1 13605 reusq0 14824 dfgcd2 15896 lcmf 15979 prmgaplem5 16393 prmgaplem6 16394 cshwshashlem2 16432 mamufacex 21002 mavmulsolcl 21162 lgsqrmodndvds 25931 2sqreultlem 26025 2sqreunnltlem 26028 uspgrn2crct 27588 2pthon3v 27724 frgrreg 28175 icceuelpart 43603 prmdvdsfmtnof1lem2 43754 lighneallem4 43782 evenprm2 43886 suppmptcfin 44434 linc1 44487 |
Copyright terms: Public domain | W3C validator |