![]() |
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 643 | . 2 ⊢ (((𝜑 ∧ 𝜓) ∧ 𝜒) ↔ (𝜓 ∧ (𝜑 ∧ 𝜒))) | |
2 | 1 | biancomi 464 | 1 ⊢ (((𝜑 ∧ 𝜓) ∧ 𝜒) ↔ ((𝜑 ∧ 𝜒) ∧ 𝜓)) |
Colors of variables: wff setvar class |
Syntax hints: ↔ wb 205 ∧ wa 397 |
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 206 df-an 398 |
This theorem is referenced by: an32s 651 3anan32 1098 indifdirOLD 4246 inrab2 4268 reupick 4279 difxp 6117 imadif 6586 respreima 7017 dff1o6 7222 dfoprab2 7416 f11o 7880 xpassen 9011 dfac5lem1 10060 kmlem3 10089 qbtwnre 13119 elioomnf 13362 modfsummod 15680 pcqcl 16729 tosso 18309 subgdmdprd 19814 pjfval2 21118 opsrtoslem1 21465 fvmptnn04if 22201 cmpcov2 22744 tx1cn 22963 tgphaus 23471 isms2 23806 elcncf1di 24261 elii1 24301 isclmp 24463 bddiblnc 25209 dvreslem 25276 dvdsflsumcom 26540 upgr2wlk 28619 upgrtrls 28652 upgristrl 28653 fusgr2wsp2nb 29281 cvnbtwn3 31233 ssmxidllem 32241 ordtconnlem1 32508 1stmbfm 32863 eulerpartlemn 32984 ballotlem2 33091 reprinrn 33234 reprdifc 33243 cusgr3cyclex 33733 dfon3 34480 brsuccf 34529 brsegle2 34697 bj-restn0b 35565 bj-opelidb1 35627 matunitlindflem2 36078 poimirlem25 36106 ftc1anc 36162 disjlem17 37264 prtlem17 37341 lcvnbtwn3 37493 cvrnbtwn3 37741 islpln5 38001 islvol5 38045 lhpexle3 38478 dibelval3 39613 dihglb2 39808 pm11.6 42679 stoweidlem17 44265 smfsuplem1 45059 |
Copyright terms: Public domain | W3C validator |