Theorem baib 920

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  921  rbaib  922  ceqsrexbv  2903  elrab3  2929  rabsn  3699  elrint2  3925  frind  4398  fnres  5391  f1ompt  5730  fliftfun  5864  ovid  6061  brdifun  6646  xpcomco  6920  isacnm  7314  ltexprlemdisj  7718  xrlenlt  8136  reapval  8648  znnnlt1  9419  difrp  9813  elfz  10135  fzolb2  10276  elfzo3  10285  fzouzsplit  10301  bitsval2  12197  rpexp  12417  isghm3  13522  isabl2  13572  dfrhm2  13858  bastop1  14497  cnntr  14639  lmres  14662  tx1cn  14683  tx2cn  14684  xmetec  14851  lgsabs1  15458