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  8904  znnnlt1  9692  difrp  10093  elfz  10417  fzolb2  10562  elfzo3  10571  fzouzsplit  10588  bitsval2  12711  rpexp  12931  ballotfilemodife  13240  isghm3  14047  isabl2  14097  dfrhm2  14461  bastop1  15184  cnntr  15326  lmres  15349  tx1cn  15370  tx2cn  15371  xmetec  15538  lgsabs1  16158