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  7560  ltexprlemdisj  7974  xrlenlt  8391  reapval  8907  znnnlt1  9697  difrp  10104  elfz  10428  fzolb2  10573  elfzo3  10582  fzouzsplit  10599  bitsval2  12730  rpexp  12951  ballotfilemodife  13292  isghm3  14100  isabl2  14181  dfrhm2  14545  bastop1  15275  cnntr  15417  lmres  15440  tx1cn  15461  tx2cn  15462  xmetec  15629  lgsabs1  16324