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  6839  xpcomco  7130  isacnm  7565  ltexprlemdisj  7979  xrlenlt  8396  reapval  8912  znnnlt1  9701  difrp  10109  elfz  10433  fzolb2  10578  elfzo3  10587  fzouzsplit  10604  bitsval2  12735  rpexp  12956  ballotfilemodife  13297  isghm3  14105  isabl2  14186  gsum2d2fi  14273  dfrhm2  14569  bastop1  15326  cnntr  15468  lmres  15491  tx1cn  15512  tx2cn  15513  xmetec  15680  lgsabs1  16380