Theorem baib 919

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  920  rbaib  921  ceqsrexbv  2869  elrab3  2895  rabsn  3660  elrint2  3886  frind  4353  fnres  5333  f1ompt  5668  fliftfun  5797  ovid  5991  brdifun  6562  xpcomco  6826  ltexprlemdisj  7605  xrlenlt  8022  reapval  8533  znnnlt1  9301  difrp  9692  elfz  10014  fzolb2  10154  elfzo3  10163  fzouzsplit  10179  rpexp  12153  isabl2  13097  bastop1  13586  cnntr  13728  lmres  13751  tx1cn  13772  tx2cn  13773  xmetec  13940  lgsabs1  14443