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 130 | . 2 | |
3 | 1, 2 | ax-mp 5 | 1 |
Colors of variables: wff set class |
Syntax hints: wb 104 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-ia1 105 ax-ia2 106 ax-ia3 107 |
This theorem depends on definitions: df-bi 116 |
This theorem is referenced by: biimpri 132 bitr2i 184 bitr3i 185 bitr4i 186 bitr3id 193 bitr3di 194 bitr4di 197 bitr4id 198 pm5.41 250 anidm 394 an21 468 pm4.87 552 anabs1 567 anabs7 569 pm4.76 599 mtbir 666 sylnibr 672 sylnbir 674 xchnxbir 676 xchbinxr 678 nbn 694 pm4.25 753 pm4.56 775 pm4.77 794 pm3.2an3 1171 syl3anbr 1277 3an6 1317 truan 1365 truimfal 1405 nottru 1408 sbid 1767 sb10f 1988 cleljust 2147 nfabdw 2331 necon3bbii 2377 rspc2gv 2846 alexeq 2856 ceqsrexbv 2861 clel2 2863 clel4 2866 dfsbcq2 2958 cbvreucsf 3113 dfdif3 3237 raldifb 3267 difab 3396 un0 3448 in0 3449 ss0b 3454 rexdifpr 3611 iindif2m 3940 epse 4327 abnex 4432 uniuni 4436 elco 4777 cotr 4992 issref 4993 mptpreima 5104 ralrnmpt 5638 rexrnmpt 5639 eroveu 6604 fprodseq 11546 toptopon 12810 xmeterval 13229 txmetcnp 13312 dedekindicclemicc 13404 eldvap 13445 if0ab 13840 bdeq 13858 bd0r 13860 bdcriota 13918 bj-d0clsepcl 13960 bj-dfom 13968 |
Copyright terms: Public domain | W3C validator |