![]() |
Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > ILE Home > Th. List > biimprcd | Unicode version |
Description: Deduce a converse commuted implication from a logical equivalence. (Contributed by NM, 3-May-1994.) (Proof shortened by Wolf Lammen, 20-Dec-2013.) |
Ref | Expression |
---|---|
biimpcd.1 |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Ref | Expression |
---|---|
biimprcd |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | id 19 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() | |
2 | biimpcd.1 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
3 | 1, 2 | syl5ibrcom 156 |
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 105 ax-ia2 106 ax-ia3 107 |
This theorem depends on definitions: df-bi 116 |
This theorem is referenced by: biimparc 297 pm5.32 449 oplem1 960 ax11i 1693 equsex 1707 eleq1a 2212 ceqsalg 2717 cgsexg 2724 cgsex2g 2725 cgsex4g 2726 ceqsex 2727 spc2egv 2779 spc3egv 2781 csbiebt 3044 dfiin2g 3854 sotricim 4253 ralxfrALT 4396 iunpw 4409 opelxp 4577 ssrel 4635 ssrel2 4637 ssrelrel 4647 iss 4873 funcnvuni 5200 fun11iun 5396 tfrlem8 6223 eroveu 6528 fundmen 6708 nneneq 6759 fidifsnen 6772 prarloclem5 7332 prarloc 7335 recexprlemss1l 7467 recexprlemss1u 7468 uzin 9382 indstr 9415 elfzmlbp 9940 |
Copyright terms: Public domain | W3C validator |