Theorem baib 921

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  922  rbaib  923  ceqsrexbv  2911  elrab3  2937  rabsn  3710  elrint2  3940  frind  4417  fnres  5412  f1ompt  5754  fliftfun  5888  ovid  6085  brdifun  6670  xpcomco  6946  isacnm  7346  ltexprlemdisj  7754  xrlenlt  8172  reapval  8684  znnnlt1  9455  difrp  9849  elfz  10171  fzolb2  10312  elfzo3  10321  fzouzsplit  10338  bitsval2  12370  rpexp  12590  isghm3  13695  isabl2  13745  dfrhm2  14031  bastop1  14670  cnntr  14812  lmres  14835  tx1cn  14856  tx2cn  14857  xmetec  15024  lgsabs1  15631