Theorem baib 920

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  921  rbaib  922  ceqsrexbv  2903  elrab3  2929  rabsn  3699  elrint2  3925  frind  4398  fnres  5391  f1ompt  5730  fliftfun  5864  ovid  6061  brdifun  6646  xpcomco  6920  isacnm  7314  ltexprlemdisj  7718  xrlenlt  8136  reapval  8648  znnnlt1  9419  difrp  9813  elfz  10135  fzolb2  10276  elfzo3  10285  fzouzsplit  10301  bitsval2  12226  rpexp  12446  isghm3  13551  isabl2  13601  dfrhm2  13887  bastop1  14526  cnntr  14668  lmres  14691  tx1cn  14712  tx2cn  14713  xmetec  14880  lgsabs1  15487