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  2891  elrab3  2917  rabsn  3685  elrint2  3911  frind  4383  fnres  5370  f1ompt  5709  fliftfun  5839  ovid  6035  brdifun  6614  xpcomco  6880  ltexprlemdisj  7666  xrlenlt  8084  reapval  8595  znnnlt1  9365  difrp  9758  elfz  10080  fzolb2  10221  elfzo3  10230  fzouzsplit  10246  rpexp  12291  isghm3  13314  isabl2  13364  dfrhm2  13650  bastop1  14251  cnntr  14393  lmres  14416  tx1cn  14437  tx2cn  14438  xmetec  14605  lgsabs1  15155