![]() |
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 157 |
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: biimparc 299 pm5.32 453 oplem1 975 ax11i 1714 equsex 1728 eleq1a 2249 ceqsalg 2766 cgsexg 2773 cgsex2g 2774 cgsex4g 2775 ceqsex 2776 spc2egv 2828 spc3egv 2830 csbiebt 3097 dfiin2g 3920 sotricim 4324 ralxfrALT 4468 iunpw 4481 opelxp 4657 ssrel 4715 ssrel2 4717 ssrelrel 4727 iss 4954 funcnvuni 5286 fun11iun 5483 tfrlem8 6319 eroveu 6626 fundmen 6806 nneneq 6857 fidifsnen 6870 prarloclem5 7499 prarloc 7502 recexprlemss1l 7634 recexprlemss1u 7635 uzin 9560 indstr 9593 elfzmlbp 10132 |
Copyright terms: Public domain | W3C validator |