![]() |
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: 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 |