Theorem baib 866

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 295	. 2 ⊢ (𝜓 → (𝜒 ↔ (𝜓 ∧ 𝜒)))
2		baib.1	. 2 ⊢ (𝜑 ↔ (𝜓 ∧ 𝜒))
3	1, 2	syl6rbbr 197	1 ⊢ (𝜓 → (𝜑 ↔ 𝜒))

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

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

This theorem depends on definitions:  df-bi 115

This theorem is referenced by:  baibr  867  rbaib  868  ceqsrexbv  2746  elrab3  2770  rabsn  3504  elrint2  3724  frind  4170  fnres  5116  f1ompt  5434  fliftfun  5557  ovid  5743  brdifun  6299  xpcomco  6522  ltexprlemdisj  7144  xrlenlt  7530  reapval  8029  znnnlt1  8768  difrp  9139  elfz  9399  fzolb2  9530  elfzo3  9539  fzouzsplit  9555  rpexp  11225