![]() |
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 156 | 1 ⊢ (𝜒 → (𝜑 → 𝜓)) |
Colors of variables: wff set class |
Syntax hints: → wi 4 ↔ wb 104 |
This theorem was proved from axioms: ax-1 5 ax-2 6 ax-mp 7 ax-ia1 105 ax-ia2 106 ax-ia3 107 |
This theorem depends on definitions: df-bi 116 |
This theorem is referenced by: biimparc 294 pm5.32 442 oplem1 922 ax11i 1650 equsex 1664 eleq1a 2160 ceqsalg 2650 cgsexg 2657 cgsex2g 2658 cgsex4g 2659 ceqsex 2660 spc2egv 2711 spc3egv 2713 csbiebt 2970 dfiin2g 3771 sotricim 4161 ralxfrALT 4304 iunpw 4317 opelxp 4483 ssrel 4541 ssrel2 4543 ssrelrel 4553 iss 4773 funcnvuni 5098 fun11iun 5289 tfrlem8 6099 eroveu 6399 fundmen 6579 nneneq 6629 fidifsnen 6642 prarloclem5 7122 prarloc 7125 recexprlemss1l 7257 recexprlemss1u 7258 uzin 9114 indstr 9144 elfzmlbp 9606 |
Copyright terms: Public domain | W3C validator |