![]() |
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 2765 cgsexg 2772 cgsex2g 2773 cgsex4g 2774 ceqsex 2775 spc2egv 2827 spc3egv 2829 csbiebt 3096 dfiin2g 3919 sotricim 4323 ralxfrALT 4467 iunpw 4480 opelxp 4656 ssrel 4714 ssrel2 4716 ssrelrel 4726 iss 4953 funcnvuni 5285 fun11iun 5482 tfrlem8 6318 eroveu 6625 fundmen 6805 nneneq 6856 fidifsnen 6869 prarloclem5 7498 prarloc 7501 recexprlemss1l 7633 recexprlemss1u 7634 uzin 9558 indstr 9591 elfzmlbp 10129 |
Copyright terms: Public domain | W3C validator |