Theorem baib 927

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  928  rbaib  929  ceqsrexbv  2948  elrab3  2974  rabsn  3756  elrint2  3990  frind  4473  fnres  5475  f1ompt  5828  fliftfun  5969  ovid  6170  brdifun  6794  xpcomco  7077  isacnm  7510  ltexprlemdisj  7921  xrlenlt  8338  reapval  8850  znnnlt1  9625  difrp  10025  elfz  10348  fzolb2  10489  elfzo3  10498  fzouzsplit  10515  bitsval2  12630  rpexp  12850  isghm3  13961  isabl2  14011  dfrhm2  14299  bastop1  14948  cnntr  15090  lmres  15113  tx1cn  15134  tx2cn  15135  xmetec  15302  lgsabs1  15912