Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > MPE Home > Th. List > an32 | Structured version Visualization version Unicode 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 681 | . 2 | |
2 | an12 838 | . 2 | |
3 | ancom 466 | . 2 | |
4 | 1, 2, 3 | 3bitri 286 | 1 |
Colors of variables: wff setvar class |
Syntax hints: wb 196 wa 384 |
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 386 |
This theorem is referenced by: an32s 846 3anan32 1050 indifdir 3883 inrab2 3900 reupick 3911 difxp 5558 resco 5639 imadif 5973 respreima 6344 dff1o6 6531 dfoprab2 6701 f11o 7128 mpt2curryd 7395 xpassen 8054 dfac5lem1 8946 kmlem3 8974 qbtwnre 12030 elioomnf 12268 modfsummod 14526 pcqcl 15561 tosso 17036 subgdmdprd 18433 opsrtoslem1 19484 pjfval2 20053 fvmptnn04if 20654 cmpcov2 21193 tx1cn 21412 tgphaus 21920 isms2 22255 elcncf1di 22698 elii1 22734 isclmp 22897 dvreslem 23673 dvdsflsumcom 24914 upgr2wlk 26564 upgrtrls 26598 upgristrl 26599 fusgr2wsp2nb 27198 cvnbtwn3 29147 ordtconnlem1 29970 1stmbfm 30322 eulerpartlemn 30443 ballotlem2 30550 reprinrn 30696 reprdifc 30705 dfon3 31999 brsuccf 32048 brsegle2 32216 bj-restn0b 33044 matunitlindflem2 33406 poimirlem25 33434 bddiblnc 33480 ftc1anc 33493 prtlem17 34161 lcvnbtwn3 34315 cvrnbtwn3 34563 islpln5 34821 islvol5 34865 lhpexle3 35298 dibelval3 36436 dihglb2 36631 pm11.6 38592 stoweidlem17 40234 smfsuplem1 41017 |
Copyright terms: Public domain | W3C validator |