Theorem baib 904

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 299	. 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-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  905  rbaib  906  ceqsrexbv  2816  elrab3  2841  rabsn  3590  elrint2  3812  frind  4274  fnres  5239  f1ompt  5571  fliftfun  5697  ovid  5887  brdifun  6456  xpcomco  6720  ltexprlemdisj  7414  xrlenlt  7829  reapval  8338  znnnlt1  9102  difrp  9480  elfz  9796  fzolb2  9931  elfzo3  9940  fzouzsplit  9956  rpexp  11831  bastop1  12252  cnntr  12394  lmres  12417  tx1cn  12438  tx2cn  12439  xmetec  12606