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  2938  elrab3  2964  rabsn  3740  elrint2  3974  frind  4455  fnres  5456  f1ompt  5806  fliftfun  5947  ovid  6148  brdifun  6772  xpcomco  7053  isacnm  7461  ltexprlemdisj  7869  xrlenlt  8286  reapval  8798  znnnlt1  9571  difrp  9971  elfz  10294  fzolb2  10435  elfzo3  10444  fzouzsplit  10461  bitsval2  12568  rpexp  12788  isghm3  13894  isabl2  13944  dfrhm2  14232  bastop1  14877  cnntr  15019  lmres  15042  tx1cn  15063  tx2cn  15064  xmetec  15231  lgsabs1  15841