Theorem baib 914

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		baib.1	. 2 |- ( ph <-> ( ps /\ ch ) )
2		ibar 299	. 2 |- ( ps -> ( ch <-> ( ps /\ ch ) ) )
3	1, 2	bitr4id 198	1 |- ( ps -> ( ph <-> ch ) )

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

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

This theorem depends on definitions:  df-bi 116

This theorem is referenced by:  baibr  915  rbaib  916  ceqsrexbv  2861  elrab3  2887  rabsn  3650  elrint2  3872  frind  4337  fnres  5314  f1ompt  5647  fliftfun  5775  ovid  5969  brdifun  6540  xpcomco  6804  ltexprlemdisj  7568  xrlenlt  7984  reapval  8495  znnnlt1  9260  difrp  9649  elfz  9971  fzolb2  10110  elfzo3  10119  fzouzsplit  10135  rpexp  12107  bastop1  12877  cnntr  13019  lmres  13042  tx1cn  13063  tx2cn  13064  xmetec  13231  lgsabs1  13734