Theorem baib 931

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 ) )

This proof depends on syntax axioms:   -> wi 4   /\ wa 104   <-> wb 105

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108

This proof depends on definitions:  df-bi 117

This theorem is used by:  baibr  932  rbaib  933  ceqsrexbv  2957  elrab3  2983  rabsn  3776  elrint2  4011  frind  4497  fnres  5500  f1ompt  5859  fliftfun  6002  ovid  6205  brdifun  6834  xpcomco  7124  isacnm  7559  ltexprlemdisj  7973  xrlenlt  8390  reapval  8906  znnnlt1  9696  difrp  10103  elfz  10427  fzolb2  10572  elfzo3  10581  fzouzsplit  10598  bitsval2  12727  rpexp  12948  ballotfilemodife  13289  isghm3  14096  isabl2  14146  dfrhm2  14510  bastop1  15233  cnntr  15375  lmres  15398  tx1cn  15419  tx2cn  15420  xmetec  15587  lgsabs1  16256