Theorem baib 862

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  863  rbaib  864  ceqsrexbv  2736  elrab3  2760  rabsn  3483  elrint2  3703  frind  4142  fnres  5081  f1ompt  5393  fliftfun  5513  ovid  5694  brdifun  6247  xpcomco  6470  ltexprlemdisj  7066  xrlenlt  7452  reapval  7951  znnnlt1  8692  difrp  9063  elfz  9323  fzolb2  9452  elfzo3  9461  fzouzsplit  9477  rpexp  10910