Theorem baib 920

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  921  rbaib  922  ceqsrexbv  2892  elrab3  2918  rabsn  3686  elrint2  3912  frind  4384  fnres  5371  f1ompt  5710  fliftfun  5840  ovid  6036  brdifun  6616  xpcomco  6882  ltexprlemdisj  7668  xrlenlt  8086  reapval  8597  znnnlt1  9368  difrp  9761  elfz  10083  fzolb2  10224  elfzo3  10233  fzouzsplit  10249  rpexp  12294  isghm3  13317  isabl2  13367  dfrhm2  13653  bastop1  14262  cnntr  14404  lmres  14427  tx1cn  14448  tx2cn  14449  xmetec  14616  lgsabs1  15196