Theorem baib 904

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		ibar 299	. 2 |- ( ps -> ( ch <-> ( ps /\ ch ) ) )
2		baib.1	. 2 |- ( ph <-> ( ps /\ ch ) )
3	1, 2	syl6rbbr 198	1 |- ( ps -> ( ph <-> ch ) )

Syntax hints:   -> wi 4   /\ wa 103   <-> wb 104

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107

This theorem depends on definitions:  df-bi 116

This theorem is referenced by:  baibr  905  rbaib  906  ceqsrexbv  2811  elrab3  2836  rabsn  3585  elrint2  3807  frind  4269  fnres  5234  f1ompt  5564  fliftfun  5690  ovid  5880  brdifun  6449  xpcomco  6713  ltexprlemdisj  7407  xrlenlt  7822  reapval  8331  znnnlt1  9095  difrp  9473  elfz  9789  fzolb2  9924  elfzo3  9933  fzouzsplit  9949  rpexp  11820  bastop1  12241  cnntr  12383  lmres  12406  tx1cn  12427  tx2cn  12428  xmetec  12595