Theorem baib 924

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  925  rbaib  926  ceqsrexbv  2934  elrab3  2960  rabsn  3733  elrint2  3963  frind  4442  fnres  5439  f1ompt  5785  fliftfun  5919  ovid  6120  brdifun  6705  xpcomco  6981  isacnm  7381  ltexprlemdisj  7789  xrlenlt  8207  reapval  8719  znnnlt1  9490  difrp  9884  elfz  10206  fzolb2  10347  elfzo3  10356  fzouzsplit  10373  bitsval2  12450  rpexp  12670  isghm3  13776  isabl2  13826  dfrhm2  14112  bastop1  14751  cnntr  14893  lmres  14916  tx1cn  14937  tx2cn  14938  xmetec  15105  lgsabs1  15712