Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > ILE Home > Th. List > biimpcd | GIF version |
Description: Deduce a commuted implication from a logical equivalence. (Contributed by NM, 3-May-1994.) (Proof shortened by Wolf Lammen, 22-Sep-2013.) |
Ref | Expression |
---|---|
biimpcd.1 | ⊢ (𝜑 → (𝜓 ↔ 𝜒)) |
Ref | Expression |
---|---|
biimpcd | ⊢ (𝜓 → (𝜑 → 𝜒)) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | id 19 | . 2 ⊢ (𝜓 → 𝜓) | |
2 | biimpcd.1 | . 2 ⊢ (𝜑 → (𝜓 ↔ 𝜒)) | |
3 | 1, 2 | syl5ibcom 144 | 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 |
This theorem depends on definitions: df-bi 110 |
This theorem is referenced by: biimpac 282 3impexpbicom 1327 ax16 1694 ax16i 1738 nelneq 2138 nelneq2 2139 nelne1 2295 nelne2 2296 spc2gv 2643 spc3gv 2645 nssne1 3001 nssne2 3002 ifbothdc 3357 difsn 3501 iununir 3738 nbrne1 3781 nbrne2 3782 mosubopt 4405 issref 4707 ssimaex 5234 chfnrn 5278 ffnfv 5323 f1elima 5412 dftpos4 5878 snon0 6356 enq0sym 6530 prop 6573 prubl 6584 0fz1 8909 elfzmlbp 8990 |
Copyright terms: Public domain | W3C validator |