Theorem baib 924

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  925  rbaib  926  ceqsrexbv  2935  elrab3  2961  rabsn  3734  elrint2  3967  frind  4447  fnres  5446  f1ompt  5794  fliftfun  5932  ovid  6133  brdifun  6724  xpcomco  7005  isacnm  7408  ltexprlemdisj  7816  xrlenlt  8234  reapval  8746  znnnlt1  9517  difrp  9917  elfz  10239  fzolb2  10380  elfzo3  10389  fzouzsplit  10406  bitsval2  12495  rpexp  12715  isghm3  13821  isabl2  13871  dfrhm2  14158  bastop1  14797  cnntr  14939  lmres  14962  tx1cn  14983  tx2cn  14984  xmetec  15151  lgsabs1  15758