Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > MPE Home > Th. List > 3ancoma | Structured version Visualization version GIF version |
Description: Commutation law for triple conjunction. (Contributed by NM, 21-Apr-1994.) (Proof shortened by Wolf Lammen, 5-Jun-2022.) |
Ref | Expression |
---|---|
3ancoma | ⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) ↔ (𝜓 ∧ 𝜑 ∧ 𝜒)) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | 3anan12 1098 | . 2 ⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) ↔ (𝜓 ∧ (𝜑 ∧ 𝜒))) | |
2 | 3anass 1097 | . 2 ⊢ ((𝜓 ∧ 𝜑 ∧ 𝜒) ↔ (𝜓 ∧ (𝜑 ∧ 𝜒))) | |
3 | 1, 2 | bitr4i 281 | 1 ⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) ↔ (𝜓 ∧ 𝜑 ∧ 𝜒)) |
Colors of variables: wff setvar class |
Syntax hints: ↔ wb 209 ∧ wa 399 ∧ w3a 1089 |
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 210 df-an 400 df-3an 1091 |
This theorem is referenced by: 3anrot 1102 3anrev 1103 cadcomb 1620 f13dfv 7082 suppssfifsupp 8997 elfzmlbp 13220 elfzo2 13243 pythagtriplem2 16367 pythagtrip 16384 xpsfrnel 17064 fucinv 17479 setcinv 17593 xrsdsreclb 20407 ordthaus 22278 regr1lem2 22634 xmetrtri2 23251 clmvscom 23984 hlcomb 26691 nb3grpr2 27468 nb3gr2nb 27469 rusgrnumwwlkslem 28050 ablomuldiv 28630 nvscom 28707 cnvadj 29970 iocinif 30819 fzto1st 31086 psgnfzto1st 31088 bnj312 32400 cgr3permute1 34084 lineext 34112 colinbtwnle 34154 outsideofcom 34164 linecom 34186 linerflx2 34187 cdlemg33d 38458 uunT12p3 42093 ichexmpl2 44593 rngcinv 45210 rngcinvALTV 45222 ringcinv 45261 ringcinvALTV 45285 |
Copyright terms: Public domain | W3C validator |