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 466 | 1 ⊢ (((𝜑 ∧ 𝜓) ∧ 𝜒) ↔ ((𝜑 ∧ 𝜒) ∧ 𝜓)) |
Colors of variables: wff setvar class |
Syntax hints: ↔ wb 209 ∧ wa 399 |
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 |
This theorem is referenced by: an32s 652 3anan32 1098 indifdirOLD 4174 inrab2 4194 reupick 4205 difxp 5990 imadif 6417 respreima 6837 dff1o6 7037 dfoprab2 7220 f11o 7666 xpassen 8653 dfac5lem1 9616 kmlem3 9645 qbtwnre 12668 elioomnf 12911 modfsummod 15235 pcqcl 16286 tosso 17755 subgdmdprd 19268 pjfval2 20518 opsrtoslem1 20859 fvmptnn04if 21593 cmpcov2 22134 tx1cn 22353 tgphaus 22861 isms2 23196 elcncf1di 23640 elii1 23680 isclmp 23842 bddiblnc 24586 dvreslem 24653 dvdsflsumcom 25917 upgr2wlk 27602 upgrtrls 27635 upgristrl 27636 fusgr2wsp2nb 28263 cvnbtwn3 30215 ssmxidllem 31205 ordtconnlem1 31438 1stmbfm 31789 eulerpartlemn 31910 ballotlem2 32017 reprinrn 32160 reprdifc 32169 cusgr3cyclex 32661 dfon3 33824 brsuccf 33873 brsegle2 34041 bj-restn0b 34872 bj-opelidb1 34934 matunitlindflem2 35386 poimirlem25 35414 ftc1anc 35470 prtlem17 36502 lcvnbtwn3 36654 cvrnbtwn3 36902 islpln5 37161 islvol5 37205 lhpexle3 37638 dibelval3 38773 dihglb2 38968 pm11.6 41532 stoweidlem17 43084 smfsuplem1 43867 |
Copyright terms: Public domain | W3C validator |