Metamath Proof Explorer

Theorem baibr

Description: Move conjunction outside of biconditional. (Contributed by NM, 11-Jul-1994)

Ref Expression
Hypothesis baib.1 
|- ( ph <-> ( ps /\ ch ) )
Assertion baibr 
|- ( ps -> ( ch <-> ph ) )

Proof

Step Hyp Ref Expression
1 baib.1 
 |-  ( ph <-> ( ps /\ ch ) )
2 1 baib 
 |-  ( ps -> ( ph <-> ch ) )
3 2 bicomd 
 |-  ( ps -> ( ch <-> ph ) )