john7rv

A⇒BとB⇒Aが両方導ければ⇔を導入できます
　　A⇒B　　B⇒A
ーーーーーーーーーーーー　⇔I
　　　　A⇔B

A⇔Bが成り立つならば
AかBの片方を結論として導出できます
　　　A⇔B
ーーーーーーーーーー　⇔E
　　　　A

　　　A⇔B
ーーーーーーーーーー　⇔E
　　　　B

同値は連言の形に変形できるので
A⇔B　⇔　(A⇒B)∧(B⇒A)
その連言の形から連言除去をすれば
⇒の形に変形できます
　　　　A⇔B
ーーーーーーーーーー　∧E
　　　(A⇒B)


　　　　A⇔B
ーーーーーーーーーー　∧E
　　　(B⇒A)