Theorem baib 827

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 285	. 2 |- (ps -> (ch <-> (ps /\ ch)))
2		baib.1	. 2 |- (ph <-> (ps /\ ch))
3	1, 2	syl6rbbr 188	1 |- (ps -> (ph <-> ch))

Syntax hints:   -> wi 4   /\ wa 97   <-> wb 98

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 99  ax-ia2 100  ax-ia3 101

This theorem depends on definitions:  df-bi 110

This theorem is referenced by:  baibr  828  rbaib  829  ceqsrexbv  2669  elrab3  2693  dfpss3  3024  rabsn  3428  elrint2  3647  fnres  4958  f1ompt  5263  fliftfun  5379  ovid  5559  brdifun  6069  xpcomco  6236  ltexprlemdisj  6580  xrlenlt  6881  reapval  7360  znnnlt1  8069  difrp  8394  elfz  8650  fzolb2  8780  elfzo3  8789  fzouzsplit  8805