Theorem baib 921

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  922  rbaib  923  ceqsrexbv  2908  elrab3  2934  rabsn  3705  elrint2  3935  frind  4412  fnres  5407  f1ompt  5749  fliftfun  5883  ovid  6080  brdifun  6665  xpcomco  6941  isacnm  7341  ltexprlemdisj  7749  xrlenlt  8167  reapval  8679  znnnlt1  9450  difrp  9844  elfz  10166  fzolb2  10307  elfzo3  10316  fzouzsplit  10333  bitsval2  12340  rpexp  12560  isghm3  13665  isabl2  13715  dfrhm2  14001  bastop1  14640  cnntr  14782  lmres  14805  tx1cn  14826  tx2cn  14827  xmetec  14994  lgsabs1  15601