Discrete Mathematics -Propositional Logic How to get 
B↔C from B∧C . Using derivation method i.e Step by Step .


My attempt :
            i) B∧C Rule P 
            ii)B Rule T (i) Simplification B∧C ⇒ B
            iii)C Rule T (i) Simplification B∧C ⇒ C

I'm stuck here ..
 A: HINT (first 3 lines):


*

*Suppose $B\land C$

*Suppose $B$

*$C$  (from 1)
A: I assume you have a natural deduction system in mind:
Goal: Derive $B \leftrightarrow C$ from the set of premises $\{B \wedge C\}$, in symbols:

$B \wedge C \vdash B \leftrightarrow C.$

Recall that for deriving a biconditional $\phi \leftrightarrow \psi$ we first have to show that a conditional holds in both sides,

$\vdash \phi \rightarrow \psi$ and $\vdash \psi \rightarrow \phi.$

Hence, our new goal is derive both $B \rightarrow C$ and $C \rightarrow B$. Let's first obtain the former.
Since we want to obtain a conditional $B \rightarrow C$, we (i) assume the antecedent $B$ as a hypothesis, (ii) derive the consequent under this assumption, (iii) use the conditional introduction rule to conclude that $B$ implies $C$:



*

*$B$, H

*$B \wedge C$, P

*$C$, 2 $\land$E (Rule called Conjunction Elimination)




*$B \to C$, 1-3 $\to$I (Conditional Introduction)


Now we do the same to obtain $C \to B$




*$C$, H

*$B \wedge C$, P

*$B$, 6 $\land$E (Conjunction Elimination)




*$C \to B$, 5-7 $\to$I (Conditional Introduction)


and we use lines 4 and 8 to get a biconditional:



*$C \leftrightarrow B$, 4, 8 $\leftrightarrow$I (Rule called Biconditional Introduction)


Now let's put all the steps together:



*

*$B$, H

*$B \wedge C$, P

*$C$, 2 $\land$E




*$B \to C$, 1-3 $\to$I




*$C$, H

*$B \wedge C$, P

*$B$, 6 $\land$E




*$C \to B$, 5-7 $\to$I

*$C \leftrightarrow B$, 4, 8 $\leftrightarrow$I


Did you get the idea?
A: I use Lukasiewicz/Polish notation and condensed detachment.  The axioms I will use are:


*

*CpCqp.

*CKpqp.

*CKpqq.

*CCpqCCqpEpq.


Here we go:
assumption 5 Kbc.
D2.5       6 b.
D1.6       7 Cqb.
D3.5       8 c.
D1.8       9 Cqc.
D4.9      10 CCcqEqc.
D10.7     11 Ebc.

