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  2883  elrab3  2909  rabsn  3674  elrint2  3900  frind  4370  fnres  5351  f1ompt  5688  fliftfun  5818  ovid  6013  brdifun  6586  xpcomco  6852  ltexprlemdisj  7635  xrlenlt  8052  reapval  8563  znnnlt1  9331  difrp  9722  elfz  10044  fzolb2  10184  elfzo3  10193  fzouzsplit  10209  rpexp  12185  isghm3  13183  isabl2  13233  dfrhm2  13504  bastop1  14043  cnntr  14185  lmres  14208  tx1cn  14229  tx2cn  14230  xmetec  14397  lgsabs1  14901