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 146 | 1 |
Colors of variables: wff set class |
Syntax hints: wi 4 wb 98 |
This theorem was proved from axioms: ax-1 5 ax-2 6 ax-mp 7 ax-ia1 99 ax-ia2 100 ax-ia3 101 |
This theorem depends on definitions: df-bi 110 |
This theorem is referenced by: biimparc 283 pm5.32 426 oplem1 882 ax11i 1602 equsex 1616 eleq1a 2109 ceqsalg 2582 cgsexg 2589 cgsex2g 2590 cgsex4g 2591 ceqsex 2592 spc2egv 2642 spc3egv 2644 csbiebt 2886 dfiin2g 3690 sotricim 4060 ralxfrALT 4199 iunpw 4211 opelxp 4374 ssrel 4428 ssrel2 4430 ssrelrel 4440 iss 4654 funcnvuni 4968 fun11iun 5147 tfrlem8 5934 eroveu 6197 fundmen 6286 nneneq 6320 fidifsnen 6331 prarloclem5 6598 prarloc 6601 recexprlemss1l 6733 recexprlemss1u 6734 uzin 8505 indstr 8536 elfzmlbp 8990 |
Copyright terms: Public domain | W3C validator |