Theorem baib 885

Description: Move conjunction outside of biconditional. (Contributed by NM, 13-May-1999.)

Hypothesis

Ref	Expression
baib.1	⊢ (𝜑 ↔ (𝜓 ∧ 𝜒))

Assertion

Ref	Expression
baib	⊢ (𝜓 → (𝜑 ↔ 𝜒))

Proof of Theorem baib

Step	Hyp	Ref	Expression
1		ibar 297	. 2 ⊢ (𝜓 → (𝜒 ↔ (𝜓 ∧ 𝜒)))
2		baib.1	. 2 ⊢ (𝜑 ↔ (𝜓 ∧ 𝜒))
3	1, 2	syl6rbbr 198	1 ⊢ (𝜓 → (𝜑 ↔ 𝜒))

Syntax hints:   → wi 4   ∧ wa 103   ↔ wb 104

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

This theorem depends on definitions:  df-bi 116

This theorem is referenced by:  baibr  886  rbaib  887  ceqsrexbv  2784  elrab3  2808  rabsn  3554  elrint2  3776  frind  4232  fnres  5195  f1ompt  5523  fliftfun  5649  ovid  5839  brdifun  6408  xpcomco  6671  ltexprlemdisj  7356  xrlenlt  7747  reapval  8250  znnnlt1  9000  difrp  9373  elfz  9683  fzolb2  9818  elfzo3  9827  fzouzsplit  9843  rpexp  11671  bastop1  12089  cnntr  12230  lmres  12253  tx1cn  12274  tx2cn  12275  xmetec  12420