Theorem baib 926

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  927  rbaib  928  ceqsrexbv  2937  elrab3  2963  rabsn  3736  elrint2  3969  frind  4449  fnres  5449  f1ompt  5798  fliftfun  5936  ovid  6137  brdifun  6728  xpcomco  7009  isacnm  7417  ltexprlemdisj  7825  xrlenlt  8243  reapval  8755  znnnlt1  9526  difrp  9926  elfz  10248  fzolb2  10389  elfzo3  10398  fzouzsplit  10415  bitsval2  12504  rpexp  12724  isghm3  13830  isabl2  13880  dfrhm2  14167  bastop1  14806  cnntr  14948  lmres  14971  tx1cn  14992  tx2cn  14993  xmetec  15160  lgsabs1  15767