Theorem baib 905

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  906  rbaib  907  ceqsrexbv  2843  elrab3  2869  rabsn  3626  elrint2  3848  frind  4311  fnres  5283  f1ompt  5615  fliftfun  5741  ovid  5931  brdifun  6500  xpcomco  6764  ltexprlemdisj  7509  xrlenlt  7925  reapval  8434  znnnlt1  9198  difrp  9581  elfz  9900  fzolb2  10035  elfzo3  10044  fzouzsplit  10060  rpexp  12007  bastop1  12443  cnntr  12585  lmres  12608  tx1cn  12629  tx2cn  12630  xmetec  12797