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  2895  elrab3  2921  rabsn  3690  elrint2  3916  frind  4388  fnres  5377  f1ompt  5716  fliftfun  5846  ovid  6043  brdifun  6628  xpcomco  6894  isacnm  7286  ltexprlemdisj  7690  xrlenlt  8108  reapval  8620  znnnlt1  9391  difrp  9784  elfz  10106  fzolb2  10247  elfzo3  10256  fzouzsplit  10272  bitsval2  12126  rpexp  12346  isghm3  13450  isabl2  13500  dfrhm2  13786  bastop1  14403  cnntr  14545  lmres  14568  tx1cn  14589  tx2cn  14590  xmetec  14757  lgsabs1  15364