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 640 | . 2 ⊢ (((𝜑 ∧ 𝜓) ∧ 𝜒) ↔ (𝜓 ∧ (𝜑 ∧ 𝜒))) | |
2 | 1 | biancomi 463 | 1 ⊢ (((𝜑 ∧ 𝜓) ∧ 𝜒) ↔ ((𝜑 ∧ 𝜒) ∧ 𝜓)) |
Colors of variables: wff setvar class |
Syntax hints: ↔ wb 207 ∧ wa 396 |
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 208 df-an 397 |
This theorem is referenced by: an32s 648 3anan32 1089 indifdir 4257 inrab2 4273 reupick 4284 difxp 6014 imadif 6431 respreima 6828 dff1o6 7023 dfoprab2 7201 f11o 7637 xpassen 8599 dfac5lem1 9537 kmlem3 9566 qbtwnre 12580 elioomnf 12820 modfsummod 15137 pcqcl 16181 tosso 17634 subgdmdprd 19085 opsrtoslem1 20192 pjfval2 20781 fvmptnn04if 21385 cmpcov2 21926 tx1cn 22145 tgphaus 22652 isms2 22987 elcncf1di 23430 elii1 23466 isclmp 23628 dvreslem 24434 dvdsflsumcom 25692 upgr2wlk 27377 upgrtrls 27410 upgristrl 27411 fusgr2wsp2nb 28040 cvnbtwn3 29992 ordtconnlem1 31066 1stmbfm 31417 eulerpartlemn 31538 ballotlem2 31645 reprinrn 31788 reprdifc 31797 cusgr3cyclex 32280 dfon3 33250 brsuccf 33299 brsegle2 33467 bj-restn0b 34276 bj-opelidb1 34337 matunitlindflem2 34770 poimirlem25 34798 bddiblnc 34843 ftc1anc 34856 prtlem17 35892 lcvnbtwn3 36044 cvrnbtwn3 36292 islpln5 36551 islvol5 36595 lhpexle3 37028 dibelval3 38163 dihglb2 38358 pm11.6 40601 stoweidlem17 42179 smfsuplem1 42962 |
Copyright terms: Public domain | W3C validator |