Metamath Proof Explorer


Theorem rbaib

Description: Move conjunction outside of biconditional. (Contributed by Mario Carneiro, 11-Sep-2015) (Proof shortened by Wolf Lammen, 19-Jan-2020)

Ref Expression
Hypothesis baib.1 φψχ
Assertion rbaib χφψ

Proof

Step Hyp Ref Expression
1 baib.1 φψχ
2 1 rbaibr χψφ
3 2 bicomd χφψ