![]() |
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 155 | 1 ⊢ (𝜒 → (𝜑 → 𝜓)) |
Colors of variables: wff set class |
Syntax hints: → wi 4 ↔ wb 103 |
This theorem was proved from axioms: ax-1 5 ax-2 6 ax-mp 7 ax-ia1 104 ax-ia2 105 ax-ia3 106 |
This theorem depends on definitions: df-bi 115 |
This theorem is referenced by: biimparc 293 pm5.32 441 oplem1 921 ax11i 1649 equsex 1663 eleq1a 2159 ceqsalg 2647 cgsexg 2654 cgsex2g 2655 cgsex4g 2656 ceqsex 2657 spc2egv 2708 spc3egv 2710 csbiebt 2967 dfiin2g 3763 sotricim 4150 ralxfrALT 4289 iunpw 4302 opelxp 4467 ssrel 4526 ssrel2 4528 ssrelrel 4538 iss 4758 funcnvuni 5083 fun11iun 5274 tfrlem8 6083 eroveu 6381 fundmen 6521 nneneq 6571 fidifsnen 6584 prarloclem5 7057 prarloc 7060 recexprlemss1l 7192 recexprlemss1u 7193 uzin 9049 indstr 9079 elfzmlbp 9539 |
Copyright terms: Public domain | W3C validator |