Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > MPE Home > Th. List > 3ancomb | Structured version Visualization version GIF version |
Description: Commutation law for triple conjunction. (Contributed by NM, 21-Apr-1994.) |
Ref | Expression |
---|---|
3ancomb | ⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) ↔ (𝜑 ∧ 𝜒 ∧ 𝜓)) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | 3ancoma 1038 | . 2 ⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) ↔ (𝜓 ∧ 𝜑 ∧ 𝜒)) | |
2 | 3anrot 1036 | . 2 ⊢ ((𝜓 ∧ 𝜑 ∧ 𝜒) ↔ (𝜑 ∧ 𝜒 ∧ 𝜓)) | |
3 | 1, 2 | bitri 263 | 1 ⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) ↔ (𝜑 ∧ 𝜒 ∧ 𝜓)) |
Colors of variables: wff setvar class |
Syntax hints: ↔ wb 195 ∧ w3a 1031 |
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 196 df-an 385 df-3an 1033 |
This theorem is referenced by: 3simpb 1052 an33rean 1438 elioore 12076 leexp2 12777 swrdswrd 13312 pcgcd 15420 ablsubsub23 18053 xmetrtri 21970 phtpcer 22602 phtpcerOLD 22603 ishl2 22974 frgra3v 26529 numclwwlkovf2num 26612 ablo32 26787 ablodivdiv 26791 ablodiv32 26793 bnj268 30028 bnj945 30098 bnj944 30262 bnj969 30270 btwncom 31291 btwnswapid2 31295 btwnouttr 31301 cgr3permute1 31325 colinearperm1 31339 endofsegid 31362 colinbtwnle 31395 broutsideof2 31399 outsideofcom 31405 neificl 32719 lhpexle2 34314 uunTT1p1 38042 uun123 38056 smflimlem4 39660 rusgrprc 40790 av-numclwwlkovf2num 41516 alsi-no-surprise 42351 |
Copyright terms: Public domain | W3C validator |