Theorem baib 861

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

Hypothesis

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

Assertion

Ref	Expression
baib	|- ( ps -> ( ph <-> ch ) )

Proof of Theorem baib

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

Syntax hints:   -> wi 4   /\ wa 102   <-> wb 103

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 104  ax-ia2 105  ax-ia3 106

This theorem depends on definitions:  df-bi 115

This theorem is referenced by:  baibr  862  rbaib  863  ceqsrexbv  2726  elrab3  2750  rabsn  3459  elrint2  3677  frind  4107  fnres  5035  f1ompt  5341  fliftfun  5456  ovid  5637  brdifun  6156  xpcomco  6323  ltexprlemdisj  6796  xrlenlt  7177  reapval  7676  znnnlt1  8399  difrp  8770  elfz  9035  fzolb2  9163  elfzo3  9172  fzouzsplit  9188  rpexp  10532