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 641 | . 2 ⊢ (((𝜑 ∧ 𝜓) ∧ 𝜒) ↔ (𝜓 ∧ (𝜑 ∧ 𝜒))) | |
2 | 1 | biancomi 463 | 1 ⊢ (((𝜑 ∧ 𝜓) ∧ 𝜒) ↔ ((𝜑 ∧ 𝜒) ∧ 𝜓)) |
Colors of variables: wff setvar class |
Syntax hints: ↔ wb 205 ∧ 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 206 df-an 397 |
This theorem is referenced by: an32s 649 3anan32 1096 indifdirOLD 4220 inrab2 4242 reupick 4253 difxp 6072 imadif 6525 respreima 6952 dff1o6 7156 dfoprab2 7342 f11o 7798 xpassen 8862 dfac5lem1 9888 kmlem3 9917 qbtwnre 12942 elioomnf 13185 modfsummod 15515 pcqcl 16566 tosso 18146 subgdmdprd 19646 pjfval2 20925 opsrtoslem1 21271 fvmptnn04if 22007 cmpcov2 22550 tx1cn 22769 tgphaus 23277 isms2 23612 elcncf1di 24067 elii1 24107 isclmp 24269 bddiblnc 25015 dvreslem 25082 dvdsflsumcom 26346 upgr2wlk 28045 upgrtrls 28078 upgristrl 28079 fusgr2wsp2nb 28707 cvnbtwn3 30659 ssmxidllem 31650 ordtconnlem1 31883 1stmbfm 32236 eulerpartlemn 32357 ballotlem2 32464 reprinrn 32607 reprdifc 32616 cusgr3cyclex 33107 dfon3 34203 brsuccf 34252 brsegle2 34420 bj-restn0b 35271 bj-opelidb1 35333 matunitlindflem2 35783 poimirlem25 35811 ftc1anc 35867 prtlem17 36897 lcvnbtwn3 37049 cvrnbtwn3 37297 islpln5 37556 islvol5 37600 lhpexle3 38033 dibelval3 39168 dihglb2 39363 pm11.6 42017 stoweidlem17 43565 smfsuplem1 44355 |
Copyright terms: Public domain | W3C validator |