Theorem baib 927

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  928  rbaib  929  ceqsrexbv  2950  elrab3  2976  rabsn  3758  elrint2  3992  frind  4475  fnres  5477  f1ompt  5830  fliftfun  5971  ovid  6172  brdifun  6796  xpcomco  7079  isacnm  7512  ltexprlemdisj  7926  xrlenlt  8343  reapval  8855  znnnlt1  9630  difrp  10031  elfz  10354  fzolb2  10496  elfzo3  10505  fzouzsplit  10522  bitsval2  12638  rpexp  12858  ballotfilemodife  13162  isghm3  13982  isabl2  14032  dfrhm2  14321  bastop1  14997  cnntr  15139  lmres  15162  tx1cn  15183  tx2cn  15184  xmetec  15351  lgsabs1  15961