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  4443  fnres  5440  f1ompt  5788  fliftfun  5926  ovid  6127  brdifun  6715  xpcomco  6993  isacnm  7393  ltexprlemdisj  7801  xrlenlt  8219  reapval  8731  znnnlt1  9502  difrp  9896  elfz  10218  fzolb2  10359  elfzo3  10368  fzouzsplit  10385  bitsval2  12463  rpexp  12683  isghm3  13789  isabl2  13839  dfrhm2  14126  bastop1  14765  cnntr  14907  lmres  14930  tx1cn  14951  tx2cn  14952  xmetec  15119  lgsabs1  15726