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  2951  elrab3  2977  rabsn  3761  elrint2  3995  frind  4478  fnres  5480  f1ompt  5833  fliftfun  5975  ovid  6178  brdifun  6807  xpcomco  7090  isacnm  7523  ltexprlemdisj  7937  xrlenlt  8354  reapval  8868  znnnlt1  9645  difrp  10046  elfz  10370  fzolb2  10514  elfzo3  10523  fzouzsplit  10540  bitsval2  12659  rpexp  12879  ballotfilemodife  13188  isghm3  14001  isabl2  14051  dfrhm2  14403  bastop1  15078  cnntr  15220  lmres  15243  tx1cn  15264  tx2cn  15265  xmetec  15432  lgsabs1  16042