Theorem baib 914

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		baib.1	. 2 ⊢ (𝜑 ↔ (𝜓 ∧ 𝜒))
2		ibar 299	. 2 ⊢ (𝜓 → (𝜒 ↔ (𝜓 ∧ 𝜒)))
3	1, 2	bitr4id 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  915  rbaib  916  ceqsrexbv  2861  elrab3  2887  rabsn  3648  elrint2  3870  frind  4335  fnres  5312  f1ompt  5644  fliftfun  5772  ovid  5966  brdifun  6536  xpcomco  6800  ltexprlemdisj  7555  xrlenlt  7971  reapval  8482  znnnlt1  9247  difrp  9636  elfz  9958  fzolb2  10097  elfzo3  10106  fzouzsplit  10122  rpexp  12094  bastop1  12836  cnntr  12978  lmres  13001  tx1cn  13022  tx2cn  13023  xmetec  13190  lgsabs1  13693