Theorem baib 927

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  928  rbaib  929  ceqsrexbv  2951  elrab3  2977  rabsn  3761  elrint2  3995  frind  4478  fnres  5480  f1ompt  5833  fliftfun  5975  ovid  6178  brdifun  6807  xpcomco  7090  isacnm  7523  ltexprlemdisj  7937  xrlenlt  8354  reapval  8867  znnnlt1  9642  difrp  10043  elfz  10367  fzolb2  10511  elfzo3  10520  fzouzsplit  10537  bitsval2  12655  rpexp  12875  ballotfilemodife  13184  isghm3  13997  isabl2  14047  dfrhm2  14399  bastop1  15074  cnntr  15216  lmres  15239  tx1cn  15260  tx2cn  15261  xmetec  15428  lgsabs1  16038