Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > MPE Home > Th. List > 3ancomb | Structured version Visualization version Unicode version |
Description: Commutation law for triple conjunction. (Contributed by NM, 21-Apr-1994.) |
Ref | Expression |
---|---|
3ancomb |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | 3ancoma 1045 | . 2 | |
2 | 3anrot 1043 | . 2 | |
3 | 1, 2 | bitri 264 | 1 |
Colors of variables: wff setvar class |
Syntax hints: wb 196 w3a 1037 |
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 197 df-an 386 df-3an 1039 |
This theorem is referenced by: 3simpb 1059 an33rean 1446 elioore 12205 leexp2 12915 swrdswrd 13460 pcgcd 15582 ablsubsub23 18230 xmetrtri 22160 phtpcer 22794 phtpcerOLD 22795 ishl2 23166 rusgrprc 26486 numclwwlkovf2num 27218 ablo32 27403 ablodivdiv 27407 ablodiv32 27409 bnj268 30775 bnj945 30844 bnj944 31008 bnj969 31016 btwncom 32121 btwnswapid2 32125 btwnouttr 32131 cgr3permute1 32155 colinearperm1 32169 endofsegid 32192 colinbtwnle 32225 broutsideof2 32229 outsideofcom 32235 neificl 33549 lhpexle2 35296 uunTT1p1 39021 uun123 39035 smflimlem4 40982 alsi-no-surprise 42542 |
Copyright terms: Public domain | W3C validator |