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 679 | . 2 ⊢ (((𝜑 ∧ 𝜓) ∧ 𝜒) ↔ (𝜑 ∧ (𝜓 ∧ 𝜒))) | |
2 | an12 834 | . 2 ⊢ ((𝜑 ∧ (𝜓 ∧ 𝜒)) ↔ (𝜓 ∧ (𝜑 ∧ 𝜒))) | |
3 | ancom 465 | . 2 ⊢ ((𝜓 ∧ (𝜑 ∧ 𝜒)) ↔ ((𝜑 ∧ 𝜒) ∧ 𝜓)) | |
4 | 1, 2, 3 | 3bitri 285 | 1 ⊢ (((𝜑 ∧ 𝜓) ∧ 𝜒) ↔ ((𝜑 ∧ 𝜒) ∧ 𝜓)) |
Colors of variables: wff setvar class |
Syntax hints: ↔ wb 195 ∧ 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 196 df-an 385 |
This theorem is referenced by: an32s 842 3anan32 1043 indifdir 3842 inrab2 3859 reupick 3870 difxp 5477 resco 5556 imadif 5887 respreima 6252 dff1o6 6431 dfoprab2 6599 f11o 7021 mpt2curryd 7282 xpassen 7939 dfac5lem1 8829 kmlem3 8857 qbtwnre 11904 elioomnf 12139 modfsummod 14367 pcqcl 15399 tosso 16859 subgdmdprd 18256 opsrtoslem1 19305 pjfval2 19872 fvmptnn04if 20473 cmpcov2 21003 tx1cn 21222 tgphaus 21730 isms2 22065 elcncf1di 22506 elii1 22542 isclmp 22705 dvreslem 23479 dvdsflsumcom 24714 is2wlk 26095 cvnbtwn3 28531 ordtconlem1 29298 1stmbfm 29649 eulerpartlemn 29770 ballotlem2 29877 dfon3 31169 brsuccf 31218 brsegle2 31386 bj-restn0b 32225 matunitlindflem2 32576 poimirlem25 32604 bddiblnc 32650 ftc1anc 32663 prtlem17 33179 lcvnbtwn3 33333 cvrnbtwn3 33581 islpln5 33839 islvol5 33883 lhpexle3 34316 dibelval3 35454 dihglb2 35649 pm11.6 37614 stoweidlem17 38910 upgr2wlk 40876 upgrtrls 40909 upgristrl 40910 |
Copyright terms: Public domain | W3C validator |