![]() |
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 | anass 682 | . 2 ⊢ (((𝜑 ∧ 𝜓) ∧ 𝜒) ↔ (𝜑 ∧ (𝜓 ∧ 𝜒))) | |
2 | an12 855 | . 2 ⊢ ((𝜑 ∧ (𝜓 ∧ 𝜒)) ↔ (𝜓 ∧ (𝜑 ∧ 𝜒))) | |
3 | ancom 465 | . 2 ⊢ ((𝜓 ∧ (𝜑 ∧ 𝜒)) ↔ ((𝜑 ∧ 𝜒) ∧ 𝜓)) | |
4 | 1, 2, 3 | 3bitri 286 | 1 ⊢ (((𝜑 ∧ 𝜓) ∧ 𝜒) ↔ ((𝜑 ∧ 𝜒) ∧ 𝜓)) |
Colors of variables: wff setvar class |
Syntax hints: ↔ wb 196 ∧ wa 383 |
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 197 df-an 385 |
This theorem is referenced by: an32s 863 3anan32 1068 indifdir 3916 inrab2 3933 reupick 3944 difxp 5593 resco 5677 imadif 6011 respreima 6384 dff1o6 6571 dfoprab2 6743 f11o 7170 mpt2curryd 7440 xpassen 8095 dfac5lem1 8984 kmlem3 9012 qbtwnre 12068 elioomnf 12306 modfsummod 14570 pcqcl 15608 tosso 17083 subgdmdprd 18479 opsrtoslem1 19532 pjfval2 20101 fvmptnn04if 20702 cmpcov2 21241 tx1cn 21460 tgphaus 21967 isms2 22302 elcncf1di 22745 elii1 22781 isclmp 22943 dvreslem 23718 dvdsflsumcom 24959 upgr2wlk 26620 upgrtrls 26654 upgristrl 26655 fusgr2wsp2nb 27314 cvnbtwn3 29275 ordtconnlem1 30098 1stmbfm 30450 eulerpartlemn 30571 ballotlem2 30678 reprinrn 30824 reprdifc 30833 dfon3 32124 brsuccf 32173 brsegle2 32341 bj-restn0b 33169 matunitlindflem2 33536 poimirlem25 33564 bddiblnc 33610 ftc1anc 33623 prtlem17 34480 lcvnbtwn3 34633 cvrnbtwn3 34881 islpln5 35139 islvol5 35183 lhpexle3 35616 dibelval3 36753 dihglb2 36948 pm11.6 38909 stoweidlem17 40552 smfsuplem1 41338 |
Copyright terms: Public domain | W3C validator |