Theorem baib 924

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  925  rbaib  926  ceqsrexbv  2934  elrab3  2960  rabsn  3733  elrint2  3964  frind  4444  fnres  5443  f1ompt  5791  fliftfun  5929  ovid  6130  brdifun  6720  xpcomco  6998  isacnm  7401  ltexprlemdisj  7809  xrlenlt  8227  reapval  8739  znnnlt1  9510  difrp  9905  elfz  10227  fzolb2  10368  elfzo3  10377  fzouzsplit  10394  bitsval2  12476  rpexp  12696  isghm3  13802  isabl2  13852  dfrhm2  14139  bastop1  14778  cnntr  14920  lmres  14943  tx1cn  14964  tx2cn  14965  xmetec  15132  lgsabs1  15739