| Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
||
| Mirrors > Home > MPE Home > Th. List > an32 | Structured version Visualization version GIF version | ||
| Description: A rearrangement of conjuncts. (Contributed by NM, 12-Mar-1995.) (Proof shortened by Wolf Lammen, 25-Dec-2012.) |
| Ref | Expression |
|---|---|
| an32 | ⊢ (((𝜑 ∧ 𝜓) ∧ 𝜒) ↔ ((𝜑 ∧ 𝜒) ∧ 𝜓)) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | an21 644 | . 2 ⊢ (((𝜑 ∧ 𝜓) ∧ 𝜒) ↔ (𝜓 ∧ (𝜑 ∧ 𝜒))) | |
| 2 | 1 | biancomi 462 | 1 ⊢ (((𝜑 ∧ 𝜓) ∧ 𝜒) ↔ ((𝜑 ∧ 𝜒) ∧ 𝜓)) |
| Colors of variables: wff setvar class |
| Syntax hints: ↔ wb 206 ∧ wa 395 |
| 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 207 df-an 396 |
| This theorem is referenced by: an32s 652 3anan32 1097 inrab2 4317 reupick 4329 difxp 6184 imadif 6650 respreima 7086 dff1o6 7295 dfoprab2 7491 f11o 7971 xpassen 9106 dfac5lem1 10163 kmlem3 10193 qbtwnre 13241 elioomnf 13484 modfsummod 15830 pcqcl 16894 tosso 18464 subgdmdprd 20054 pjfval2 21729 opsrtoslem1 22079 fvmptnn04if 22855 cmpcov2 23398 tx1cn 23617 tgphaus 24125 isms2 24460 elcncf1di 24921 elii1 24964 isclmp 25130 bddiblnc 25877 dvreslem 25944 dvdsflsumcom 27231 upgr2wlk 29686 upgrtrls 29719 upgristrl 29720 fusgr2wsp2nb 30353 cvnbtwn3 32307 an42ds 32469 an52ds 32470 an62ds 32471 an72ds 32472 an82ds 32473 fdifsupp 32694 ssdifidllem 33484 ssmxidllem 33501 ordtconnlem1 33923 1stmbfm 34262 eulerpartlemn 34383 ballotlem2 34491 reprinrn 34633 reprdifc 34642 cusgr3cyclex 35141 dfon3 35893 brsuccf 35942 brsegle2 36110 bj-restn0b 37092 bj-opelidb1 37154 matunitlindflem2 37624 poimirlem25 37652 ftc1anc 37708 disjlem17 38800 prtlem17 38877 lcvnbtwn3 39029 cvrnbtwn3 39277 islpln5 39537 islvol5 39581 lhpexle3 40014 dibelval3 41149 dihglb2 41344 pm11.6 44411 stoweidlem17 46032 smfsuplem1 46826 |
| Copyright terms: Public domain | W3C validator |