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 3771 domtriomlem 10053 nn01to3 12534 xnn0lenn0nn0 12832 injresinjlem 13359 expnngt1 13805 reusq0 15023 dfgcd2 16103 lcmf 16187 prmgaplem5 16605 prmgaplem6 16606 cshwshashlem2 16647 mamufacex 21285 mavmulsolcl 21445 lgsqrmodndvds 26231 2sqreultlem 26325 2sqreunnltlem 26328 uspgrn2crct 27889 2pthon3v 28024 frgrreg 28474 icceuelpart 44559 prmdvdsfmtnof1lem2 44708 lighneallem4 44733 evenprm2 44837 suppmptcfin 45386 linc1 45437 |
Copyright terms: Public domain | W3C validator |