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  2935  elrab3  2961  rabsn  3734  elrint2  3967  frind  4447  fnres  5446  f1ompt  5794  fliftfun  5932  ovid  6133  brdifun  6724  xpcomco  7005  isacnm  7411  ltexprlemdisj  7819  xrlenlt  8237  reapval  8749  znnnlt1  9520  difrp  9920  elfz  10242  fzolb2  10383  elfzo3  10392  fzouzsplit  10409  bitsval2  12498  rpexp  12718  isghm3  13824  isabl2  13874  dfrhm2  14161  bastop1  14800  cnntr  14942  lmres  14965  tx1cn  14986  tx2cn  14987  xmetec  15154  lgsabs1  15761