Theorem baib 920

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 301	. 2 ⊢ (𝜓 → (𝜒 ↔ (𝜓 ∧ 𝜒)))
3	1, 2	bitr4id 199	1 ⊢ (𝜓 → (𝜑 ↔ 𝜒))

Syntax hints:   → wi 4   ∧ wa 104   ↔ wb 105

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

This theorem depends on definitions:  df-bi 117

This theorem is referenced by:  baibr  921  rbaib  922  ceqsrexbv  2895  elrab3  2921  rabsn  3689  elrint2  3915  frind  4387  fnres  5374  f1ompt  5713  fliftfun  5843  ovid  6039  brdifun  6619  xpcomco  6885  ltexprlemdisj  7673  xrlenlt  8091  reapval  8603  znnnlt1  9374  difrp  9767  elfz  10089  fzolb2  10230  elfzo3  10239  fzouzsplit  10255  bitsval2  12109  rpexp  12321  isghm3  13374  isabl2  13424  dfrhm2  13710  bastop1  14319  cnntr  14461  lmres  14484  tx1cn  14505  tx2cn  14506  xmetec  14673  lgsabs1  15280