| 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 559 anabs1 574 anabs7 576 an43 590 pm4.76 608 mtbir 678 sylnibr 684 sylnbir 686 xchnxbir 688 xchbinxr 690 nbn 707 pm4.25 766 pm4.56 788 pm4.77 807 pm3.2an3 1203 syl3anbr 1318 3an6 1359 truan 1415 truimfal 1455 nottru 1458 sbid 1822 sb10f 2048 cleljust 2208 eqabdv 2361 nfabdw 2394 necon3bbii 2440 rspc2gv 2923 alexeq 2933 ceqsrexbv 2938 clel2 2940 clel4 2943 dfsbcq2 3035 cbvreucsf 3193 dfdif3 3319 raldifb 3349 difab 3478 un0 3530 in0 3531 ss0b 3536 rexdifpr 3701 snssb 3811 snssg 3812 iindif2m 4043 epse 4445 abnex 4550 uniuni 4554 elco 4902 cotr 5125 issref 5126 mptpreima 5237 ralrnmpt 5797 rexrnmpt 5798 eroveu 6838 wrd2ind 11353 fprodseq 12207 issrg 14042 toptopon 14812 xmeterval 15229 txmetcnp 15312 dedekindicclemicc 15426 eldvap 15476 fsumdvdsmul 15788 isclwwlk 16318 iseupthf1o 16372 eupth2lem1 16382 bdeq 16522 bd0r 16524 bdcriota 16582 bj-d0clsepcl 16624 bj-dfom 16632 |
| Copyright terms: Public domain | W3C validator |