Theorem baib 909

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 299	. 2 |- ( ps -> ( ch <-> ( ps /\ ch ) ) )
3	1, 2	bitr4id 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  910  rbaib  911  ceqsrexbv  2857  elrab3  2883  rabsn  3643  elrint2  3865  frind  4330  fnres  5304  f1ompt  5636  fliftfun  5764  ovid  5958  brdifun  6528  xpcomco  6792  ltexprlemdisj  7547  xrlenlt  7963  reapval  8474  znnnlt1  9239  difrp  9628  elfz  9950  fzolb2  10089  elfzo3  10098  fzouzsplit  10114  rpexp  12085  bastop1  12723  cnntr  12865  lmres  12888  tx1cn  12909  tx2cn  12910  xmetec  13077  lgsabs1  13580