Theorem baib 920

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  921  rbaib  922  ceqsrexbv  2895  elrab3  2921  rabsn  3690  elrint2  3916  frind  4388  fnres  5377  f1ompt  5716  fliftfun  5846  ovid  6043  brdifun  6628  xpcomco  6894  isacnm  7288  ltexprlemdisj  7692  xrlenlt  8110  reapval  8622  znnnlt1  9393  difrp  9786  elfz  10108  fzolb2  10249  elfzo3  10258  fzouzsplit  10274  bitsval2  12128  rpexp  12348  isghm3  13452  isabl2  13502  dfrhm2  13788  bastop1  14405  cnntr  14547  lmres  14570  tx1cn  14591  tx2cn  14592  xmetec  14759  lgsabs1  15366