![]() |
Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > ILE Home > Th. List > ancom | Unicode version |
Description: Commutative law for conjunction. Theorem *4.3 of [WhiteheadRussell] p. 118. (Contributed by NM, 25-Jun-1998.) (Proof shortened by Wolf Lammen, 4-Nov-2012.) |
Ref | Expression |
---|---|
ancom |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | pm3.22 265 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
2 | pm3.22 265 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
3 | 1, 2 | impbii 126 |
1
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Colors of variables: wff set class |
Syntax hints: ![]() ![]() |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-ia1 106 ax-ia2 107 ax-ia3 108 |
This theorem depends on definitions: df-bi 117 |
This theorem is referenced by: ancomd 267 ancomsd 269 biancomi 270 biancomd 271 pm4.71r 390 pm5.32rd 451 pm5.32ri 455 anbi2ci 459 anbi12ci 461 bianassc 470 mpan10 474 an12 561 an32 562 an13 563 an42 587 andir 820 rbaib 922 rbaibr 923 3anrot 985 3ancoma 987 excxor 1389 xorcom 1399 xordc 1403 xordc1 1404 dfbi3dc 1408 ancomsimp 1451 exancom 1619 19.29r 1632 19.42h 1698 19.42 1699 eu1 2063 moaneu 2114 moanmo 2115 2eu7 2132 eq2tri 2249 r19.28av 2626 r19.29r 2628 r19.42v 2647 rexcomf 2652 rabswap 2669 euxfr2dc 2937 rmo4 2945 reu8 2948 rmo3f 2949 rmo3 3069 incom 3342 difin2 3412 symdifxor 3416 inuni 4170 eqvinop 4258 uniuni 4466 dtruex 4573 elvvv 4704 brinxp2 4708 dmuni 4852 dfres2 4974 dfima2 4987 imadmrn 4995 imai 4999 cnvxp 5062 cnvcnvsn 5120 mptpreima 5137 rnco 5150 unixpm 5179 ressn 5184 xpcom 5190 fncnv 5297 fununi 5299 imadiflem 5310 fnres 5347 fnopabg 5354 dff1o2 5481 eqfnfv3 5631 respreima 5660 fsn 5704 fliftcnv 5812 isoini 5835 spc2ed 6252 brtpos2 6270 tpostpos 6283 tposmpo 6300 nnaord 6528 pmex 6671 elpmg 6682 mapval2 6696 mapsnen 6829 map1 6830 xpsnen 6839 xpcomco 6844 elfi2 6989 supmoti 7010 cnvti 7036 2omotaplemap 7274 elni2 7331 enq0enq 7448 prltlu 7504 prnmaxl 7505 prnminu 7506 nqprrnd 7560 ltpopr 7612 letri3 8056 lesub0 8454 creur 8934 xrletri3 9822 iooneg 10006 iccneg 10007 elfzuzb 10037 fzrev 10102 redivap 10901 imdivap 10908 rersqreu 11055 lenegsq 11122 climrecvg1n 11374 fisumcom2 11464 fsumcom 11465 fprodcom2fi 11652 fprodcom 11653 gcdcom 11992 bezoutlembi 12024 dfgcd2 12033 lcmcom 12082 isprm2 12135 unennn 12416 dfrhm2 13465 issubrng 13507 ntreq0 14016 restopn2 14067 ismet2 14238 blres 14318 metrest 14390 dedekindicclemicc 14494 sincosq3sgn 14633 lgsdi 14822 |
Copyright terms: Public domain | W3C validator |