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  2947  elrab3  2973  rabsn  3755  elrint2  3989  frind  4472  fnres  5474  f1ompt  5827  fliftfun  5968  ovid  6169  brdifun  6793  xpcomco  7076  isacnm  7509  ltexprlemdisj  7917  xrlenlt  8334  reapval  8846  znnnlt1  9621  difrp  10021  elfz  10344  fzolb2  10485  elfzo3  10494  fzouzsplit  10511  bitsval2  12623  rpexp  12843  isghm3  13950  isabl2  14000  dfrhm2  14288  bastop1  14935  cnntr  15077  lmres  15100  tx1cn  15121  tx2cn  15122  xmetec  15289  lgsabs1  15899