![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
Mirrors > Home > MPE Home > Th. List > 3ancoma | Structured version Unicode version |
Description: Commutation law for triple conjunction. (Contributed by NM, 21-Apr-1994.) |
Ref | Expression |
---|---|
3ancoma |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | ancom 450 |
. . 3
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
2 | 1 | anbi1i 695 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
3 | df-3an 967 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
4 | df-3an 967 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
5 | 2, 3, 4 | 3bitr4i 277 |
1
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Colors of variables: wff setvar class |
Syntax hints: ![]() ![]() ![]() |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 |
This theorem depends on definitions: df-bi 185 df-an 371 df-3an 967 |
This theorem is referenced by: 3ancomb 974 3anrev 976 3anan12 978 3com12 1192 suppssfifsupp 7733 elfzmlbp 11589 elfzo2 11654 pythagtriplem2 13983 pythagtrip 14000 xpsfrnel 14600 fucinv 14982 setcinv 15057 xrsdsreclb 17966 ordthaus 19101 regr1lem2 19426 xmetrtri2 20044 nbgrasym 23480 nb3grapr2 23494 nb3gra2nb 23495 ablomuldiv 23908 nvadd12 24133 nvscom 24141 cnvadj 25428 iocinif 26202 cgr3permute1 28210 lineext 28238 colinbtwnle 28280 outsideofcom 28290 linecom 28312 linerflx2 28313 f13dfv 30282 iswwlk 30452 rusgranumwlklem0 30701 frgra3v 30729 uunT12p3 31832 bnj312 31997 cdlemg33d 34656 |
Copyright terms: Public domain | W3C validator |