![]() |
Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > ILE Home > Th. List > biimprcd | GIF 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: → wi 4 ↔ wb 105 |
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 977 ax11i 1725 equsex 1739 eleq1a 2261 ceqsalg 2780 cgsexg 2787 cgsex2g 2788 cgsex4g 2789 ceqsex 2790 spc2egv 2842 spc3egv 2844 csbiebt 3111 dfiin2g 3934 sotricim 4341 ralxfrALT 4485 iunpw 4498 opelxp 4674 ssrel 4732 ssrel2 4734 ssrelrel 4744 iss 4971 funcnvuni 5304 fun11iun 5501 tfrlem8 6344 eroveu 6653 fundmen 6833 nneneq 6886 fidifsnen 6899 prarloclem5 7530 prarloc 7533 recexprlemss1l 7665 recexprlemss1u 7666 uzin 9592 indstr 9625 elfzmlbp 10164 |
Copyright terms: Public domain | W3C validator |