![]() |
Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > ILE Home > Th. List > bicomi | Unicode version |
Description: Inference from commutative law for logical equivalence. (Contributed by NM, 5-Aug-1993.) (Revised by NM, 16-Sep-2013.) |
Ref | Expression |
---|---|
bicomi.1 |
![]() ![]() ![]() ![]() ![]() ![]() |
Ref | Expression |
---|---|
bicomi |
![]() ![]() ![]() ![]() ![]() ![]() |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | bicomi.1 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() | |
2 | bicom1 131 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
3 | 1, 2 | ax-mp 5 |
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: biimpri 133 bitr2i 185 bitr3i 186 bitr4i 187 bitr3id 194 bitr3di 195 bitr4di 198 bitr4id 199 pm5.41 251 anidm 396 an21 471 pm4.87 557 anabs1 572 anabs7 574 pm4.76 604 mtbir 671 sylnibr 677 sylnbir 679 xchnxbir 681 xchbinxr 683 nbn 699 pm4.25 758 pm4.56 780 pm4.77 799 pm3.2an3 1176 syl3anbr 1282 3an6 1322 truan 1370 truimfal 1410 nottru 1413 sbid 1774 sb10f 1995 cleljust 2154 nfabdw 2338 necon3bbii 2384 rspc2gv 2853 alexeq 2863 ceqsrexbv 2868 clel2 2870 clel4 2873 dfsbcq2 2965 cbvreucsf 3121 dfdif3 3245 raldifb 3275 difab 3404 un0 3456 in0 3457 ss0b 3462 rexdifpr 3620 snssb 3725 snssg 3726 iindif2m 3954 epse 4342 abnex 4447 uniuni 4451 elco 4793 cotr 5010 issref 5011 mptpreima 5122 ralrnmpt 5658 rexrnmpt 5659 eroveu 6625 fprodseq 11586 issrg 13101 toptopon 13409 xmeterval 13828 txmetcnp 13911 dedekindicclemicc 14003 eldvap 14044 if0ab 14439 bdeq 14457 bd0r 14459 bdcriota 14517 bj-d0clsepcl 14559 bj-dfom 14567 |
Copyright terms: Public domain | W3C validator |