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 pm4.87 547 anabs1 562 anabs7 564 pm4.76 594 mtbir 661 sylnibr 667 sylnbir 669 xchnxbir 671 xchbinxr 673 nbn 689 pm4.25 748 pm4.56 770 pm4.77 789 pm3.2an3 1161 syl3anbr 1264 3an6 1304 truan 1352 truimfal 1392 nottru 1395 sbid 1754 sb10f 1975 cleljust 2134 nfabdw 2318 necon3bbii 2364 rspc2gv 2828 alexeq 2838 ceqsrexbv 2843 clel2 2845 clel4 2848 dfsbcq2 2940 cbvreucsf 3095 dfdif3 3217 raldifb 3247 difab 3376 un0 3427 in0 3428 ss0b 3433 rexdifpr 3588 iindif2m 3916 epse 4302 abnex 4407 uniuni 4411 elco 4752 cotr 4967 issref 4968 mptpreima 5079 ralrnmpt 5609 rexrnmpt 5610 eroveu 6571 fprodseq 11480 toptopon 12427 xmeterval 12846 txmetcnp 12929 dedekindicclemicc 13021 eldvap 13062 if0ab 13391 bdeq 13409 bd0r 13411 bdcriota 13469 bj-d0clsepcl 13511 bj-dfom 13519 |
Copyright terms: Public domain | W3C validator |