Theorem baib 931

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 ) )

This proof depends on syntax axioms:   -> wi 4   /\ wa 104   <-> wb 105

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108

This proof depends on definitions:  df-bi 117

This theorem is used by:  baibr  932  rbaib  933  ceqsrexbv  2957  elrab3  2983  rabsn  3776  elrint2  4011  frind  4499  fnres  5503  f1ompt  5862  fliftfun  6005  ovid  6208  brdifun  6838  xpcomco  7128  isacnm  7565  ltexprlemdisj  7979  xrlenlt  8396  reapval  8912  znnnlt1  9703  difrp  10110  elfz  10434  fzolb2  10579  elfzo3  10588  fzouzsplit  10605  bitsval2  12736  rpexp  12957  ballotfilemodife  13298  isghm3  14106  isabl2  14187  gsum2d2fi  14274  dfrhm2  14570  bastop1  15309  cnntr  15451  lmres  15474  tx1cn  15495  tx2cn  15496  xmetec  15663  lgsabs1  16363