Theorem baib 926

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  927  rbaib  928  ceqsrexbv  2937  elrab3  2963  rabsn  3736  elrint2  3969  frind  4449  fnres  5449  f1ompt  5798  fliftfun  5937  ovid  6138  brdifun  6729  xpcomco  7010  isacnm  7418  ltexprlemdisj  7826  xrlenlt  8244  reapval  8756  znnnlt1  9527  difrp  9927  elfz  10249  fzolb2  10390  elfzo3  10399  fzouzsplit  10416  bitsval2  12507  rpexp  12727  isghm3  13833  isabl2  13883  dfrhm2  14171  bastop1  14810  cnntr  14952  lmres  14975  tx1cn  14996  tx2cn  14997  xmetec  15164  lgsabs1  15771