Theorem baib 931

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 ⊢ (𝜓 → (𝜑 ↔ 𝜒))

This proof depends on syntax axioms:   → wi 4   ∧ wa 104   ↔ wb 105

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108

This proof depends on definitions:  df-bi 117

This theorem is used by:  baibr  932  rbaib  933  ceqsrexbv  2957  elrab3  2983  rabsn  3776  elrint2  4011  frind  4497  fnres  5500  f1ompt  5859  fliftfun  6002  ovid  6205  brdifun  6834  xpcomco  7124  isacnm  7559  ltexprlemdisj  7973  xrlenlt  8390  reapval  8905  znnnlt1  9694  difrp  10095  elfz  10419  fzolb2  10564  elfzo3  10573  fzouzsplit  10590  bitsval2  12713  rpexp  12933  ballotfilemodife  13242  isghm3  14049  isabl2  14099  dfrhm2  14463  bastop1  15186  cnntr  15328  lmres  15351  tx1cn  15372  tx2cn  15373  xmetec  15540  lgsabs1  16170