Theorem baib 866

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  867  rbaib  868  ceqsrexbv  2748  elrab3  2772  rabsn  3509  elrint2  3729  frind  4179  fnres  5130  f1ompt  5450  fliftfun  5575  ovid  5761  brdifun  6319  xpcomco  6542  ltexprlemdisj  7165  xrlenlt  7551  reapval  8053  znnnlt1  8798  difrp  9170  elfz  9430  fzolb2  9565  elfzo3  9574  fzouzsplit  9590  rpexp  11410