Theorem baib 924

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 301	. 2 |- ( ps -> ( ch <-> ( ps /\ ch ) ) )
3	1, 2	bitr4id 199	1 |- ( ps -> ( ph <-> ch ) )

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

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

This theorem depends on definitions:  df-bi 117

This theorem is referenced by:  baibr  925  rbaib  926  ceqsrexbv  2934  elrab3  2960  rabsn  3733  elrint2  3964  frind  4443  fnres  5440  f1ompt  5788  fliftfun  5926  ovid  6127  brdifun  6715  xpcomco  6993  isacnm  7396  ltexprlemdisj  7804  xrlenlt  8222  reapval  8734  znnnlt1  9505  difrp  9900  elfz  10222  fzolb2  10363  elfzo3  10372  fzouzsplit  10389  bitsval2  12470  rpexp  12690  isghm3  13796  isabl2  13846  dfrhm2  14133  bastop1  14772  cnntr  14914  lmres  14937  tx1cn  14958  tx2cn  14959  xmetec  15126  lgsabs1  15733