Theorem baib 905

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  906  rbaib  907  ceqsrexbv  2820  elrab3  2845  rabsn  3598  elrint2  3820  frind  4282  fnres  5247  f1ompt  5579  fliftfun  5705  ovid  5895  brdifun  6464  xpcomco  6728  ltexprlemdisj  7438  xrlenlt  7853  reapval  8362  znnnlt1  9126  difrp  9509  elfz  9827  fzolb2  9962  elfzo3  9971  fzouzsplit  9987  rpexp  11867  bastop1  12291  cnntr  12433  lmres  12456  tx1cn  12477  tx2cn  12478  xmetec  12645