![]() |
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 262 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
2 | pm3.22 262 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
3 | 1, 2 | impbii 125 |
1
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Colors of variables: wff set class |
Syntax hints: ![]() ![]() |
This theorem was proved from axioms: ax-1 5 ax-2 6 ax-mp 7 ax-ia1 105 ax-ia2 106 ax-ia3 107 |
This theorem depends on definitions: df-bi 116 |
This theorem is referenced by: ancomd 264 ancomsd 266 pm4.71r 383 pm5.32rd 440 pm5.32ri 444 anbi2ci 448 anbi12ci 450 mpan10 459 an12 529 an32 530 an13 531 an42 555 andir 769 rbaib 869 rbaibr 870 3anrot 930 3ancoma 932 excxor 1315 xorcom 1325 xordc 1329 xordc1 1330 dfbi3dc 1334 ancomsimp 1375 exancom 1545 19.29r 1558 19.42h 1623 19.42 1624 eu1 1974 moaneu 2025 moanmo 2026 2eu7 2043 eq2tri 2148 r19.28av 2506 r19.29r 2508 r19.42v 2525 rexcomf 2530 rabswap 2546 euxfr2dc 2801 rmo4 2809 reu8 2812 rmo3f 2813 rmo3 2931 incom 3193 difin2 3262 symdifxor 3266 inuni 3997 eqvinop 4079 uniuni 4286 dtruex 4388 elvvv 4514 brinxp2 4518 dmuni 4659 dfres2 4777 dfima2 4789 imadmrn 4797 imai 4801 cnvxp 4863 cnvcnvsn 4920 mptpreima 4937 rnco 4950 unixpm 4979 ressn 4984 xpcom 4990 fncnv 5093 fununi 5095 imadiflem 5106 fnres 5143 fnopabg 5150 dff1o2 5271 eqfnfv3 5413 respreima 5441 fsn 5483 fliftcnv 5588 isoini 5611 spc2ed 6012 brtpos2 6030 tpostpos 6043 tposmpt2 6060 nnaord 6282 pmex 6424 elpmg 6435 mapval2 6449 mapsnen 6582 map1 6583 xpsnen 6591 xpcomco 6596 supmoti 6742 cnvti 6768 elni2 6934 enq0enq 7051 prltlu 7107 prnmaxl 7108 prnminu 7109 nqprrnd 7163 ltpopr 7215 letri3 7627 lesub0 8018 creur 8480 xrletri3 9331 iooneg 9466 iccneg 9467 elfzuzb 9495 fzrev 9559 redivap 10369 imdivap 10376 rersqreu 10522 lenegsq 10589 climrecvg1n 10798 fisumcom2 10893 fsumcom 10894 gcdcom 11304 bezoutlembi 11333 dfgcd2 11342 lcmcom 11385 isprm2 11438 unennn 11549 ntreq0 11893 |
Copyright terms: Public domain | W3C validator |