Theorem baib 926

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  927  rbaib  928  ceqsrexbv  2936  elrab3  2962  rabsn  3737  elrint2  3970  frind  4451  fnres  5451  f1ompt  5801  fliftfun  5942  ovid  6143  brdifun  6734  xpcomco  7015  isacnm  7423  ltexprlemdisj  7831  xrlenlt  8249  reapval  8761  znnnlt1  9532  difrp  9932  elfz  10254  fzolb2  10395  elfzo3  10404  fzouzsplit  10421  bitsval2  12528  rpexp  12748  isghm3  13854  isabl2  13904  dfrhm2  14192  bastop1  14836  cnntr  14978  lmres  15001  tx1cn  15022  tx2cn  15023  xmetec  15190  lgsabs1  15797