Theorem rsubj_elim
Theorem.
rsubj_elim
(A ↔ B) → B → A
Proof
01. 1 ⊢ A ↔ B,
hypo
. 02. 1 ⊢ B → A,
bij_elimr
1. rsubj_elim. ⊢ (A ↔ B) → B → A,
subj_intro
2.