Metamath Proof Explorer


Theorem baib

Description: Move conjunction outside of biconditional. (Contributed by NM, 13-May-1999)

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

Proof

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