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  4499  fnres  5503  f1ompt  5862  fliftfun  6005  ovid  6208  brdifun  6838  xpcomco  7129  isacnm  7566  ltexprlemdisj  7980  xrlenlt  8397  reapval  8913  znnnlt1  9704  difrp  10111  elfz  10435  fzolb2  10580  elfzo3  10589  fzouzsplit  10606  bitsval2  12737  rpexp  12958  ballotfilemodife  13299  isghm3  14107  isabl2  14188  gsum2d2fi  14275  dfrhm2  14571  bastop1  15321  cnntr  15463  lmres  15486  tx1cn  15507  tx2cn  15508  xmetec  15675  lgsabs1  16375