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 252 | . 2 | |
2 | pm3.22 252 | . 2 | |
3 | 1, 2 | impbii 117 | 1 |
Colors of variables: wff set class |
Syntax hints: wa 97 wb 98 |
This theorem was proved from axioms: ax-1 5 ax-2 6 ax-mp 7 ax-ia1 99 ax-ia2 100 ax-ia3 101 |
This theorem depends on definitions: df-bi 110 |
This theorem is referenced by: ancomd 254 ancomsd 256 pm4.71r 370 pm5.32rd 424 pm5.32ri 428 anbi2ci 432 anbi12ci 434 mpan10 443 an12 495 an32 496 an13 497 an42 521 andir 732 rbaib 830 rbaibr 831 3anrot 890 3ancoma 892 excxor 1269 xorcom 1279 xordc 1283 xordc1 1284 dfbi3dc 1288 ancomsimp 1329 exancom 1499 19.29r 1512 19.42h 1577 19.42 1578 eu1 1925 moaneu 1976 moanmo 1977 2eu7 1994 eq2tri 2099 r19.28av 2449 r19.29r 2451 r19.42v 2467 rexcomf 2472 rabswap 2488 euxfr2dc 2726 rmo4 2734 reu8 2737 rmo3 2849 incom 3129 difin2 3199 symdifxor 3203 inuni 3909 eqvinop 3980 uniuni 4183 dtruex 4283 elvvv 4403 brinxp2 4407 dmuni 4545 dfres2 4658 dfima2 4670 imadmrn 4678 imai 4681 cnvxp 4742 cnvcnvsn 4797 mptpreima 4814 rnco 4827 unixpm 4853 ressn 4858 xpcom 4864 fncnv 4965 fununi 4967 imadiflem 4978 fnres 5015 fnopabg 5022 dff1o2 5131 eqfnfv3 5267 respreima 5295 fsn 5335 fliftcnv 5435 isoini 5457 brtpos2 5866 tpostpos 5879 tposmpt2 5896 nnaord 6082 xpsnen 6295 xpcomco 6300 elni2 6412 enq0enq 6529 prltlu 6585 prnmaxl 6586 prnminu 6587 nqprrnd 6641 ltpopr 6693 letri3 7099 lesub0 7474 creur 7911 xrletri3 8721 iooneg 8856 iccneg 8857 elfzuzb 8884 fzrev 8946 redivap 9474 imdivap 9481 rersqreu 9626 lenegsq 9691 climrecvg1n 9867 |
Copyright terms: Public domain | W3C validator |