Theorem baib 924

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  925  rbaib  926  ceqsrexbv  2935  elrab3  2961  rabsn  3734  elrint2  3965  frind  4445  fnres  5444  f1ompt  5792  fliftfun  5930  ovid  6131  brdifun  6722  xpcomco  7003  isacnm  7406  ltexprlemdisj  7814  xrlenlt  8232  reapval  8744  znnnlt1  9515  difrp  9915  elfz  10237  fzolb2  10378  elfzo3  10387  fzouzsplit  10404  bitsval2  12492  rpexp  12712  isghm3  13818  isabl2  13868  dfrhm2  14155  bastop1  14794  cnntr  14936  lmres  14959  tx1cn  14980  tx2cn  14981  xmetec  15148  lgsabs1  15755