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

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  932  rbaib  933  ceqsrexbv  2957  elrab3  2983  rabsn  3772  elrint2  4006  frind  4492  fnres  5495  f1ompt  5850  fliftfun  5992  ovid  6195  brdifun  6824  xpcomco  7114  isacnm  7549  ltexprlemdisj  7963  xrlenlt  8380  reapval  8894  znnnlt1  9671  difrp  10072  elfz  10396  fzolb2  10540  elfzo3  10549  fzouzsplit  10566  bitsval2  12689  rpexp  12909  ballotfilemodife  13218  isghm3  14024  isabl2  14074  dfrhm2  14434  bastop1  15107  cnntr  15249  lmres  15272  tx1cn  15293  tx2cn  15294  xmetec  15461  lgsabs1  16072