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

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  932  rbaib  933  ceqsrexbv  2957  elrab3  2983  rabsn  3775  elrint2  4009  frind  4495  fnres  5498  f1ompt  5853  fliftfun  5996  ovid  6199  brdifun  6828  xpcomco  7118  isacnm  7553  ltexprlemdisj  7967  xrlenlt  8384  reapval  8898  znnnlt1  9675  difrp  10076  elfz  10400  fzolb2  10545  elfzo3  10554  fzouzsplit  10571  bitsval2  12694  rpexp  12914  ballotfilemodife  13223  isghm3  14030  isabl2  14080  dfrhm2  14444  bastop1  15167  cnntr  15309  lmres  15332  tx1cn  15353  tx2cn  15354  xmetec  15521  lgsabs1  16141