Goal: (φ↔ψ)
System: K(m)
using derived rules: false
1. K(m) ⊢ (φ→ψ)	(premise)
2. K(m) ⊢ (ψ→φ)	(premise)
3. K(m) ⊢ ((φ→ψ)→((ψ→φ)→(φ↔ψ)))	(A1)
4. K(m) ⊢ ((ψ→φ)→(φ↔ψ))	(R1:1,3)
5. K(m) ⊢ (φ↔ψ)	(R1:2,4)