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  12658  rpexp  12878  ballotfilemodife  13187  isghm3  14000  isabl2  14050  dfrhm2  14402  bastop1  15077  cnntr  15219  lmres  15242  tx1cn  15263  tx2cn  15264  xmetec  15431  lgsabs1  16041