Theorem baib 923

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  924  rbaib  925  ceqsrexbv  2914  elrab3  2940  rabsn  3713  elrint2  3943  frind  4420  fnres  5416  f1ompt  5759  fliftfun  5893  ovid  6092  brdifun  6677  xpcomco  6953  isacnm  7353  ltexprlemdisj  7761  xrlenlt  8179  reapval  8691  znnnlt1  9462  difrp  9856  elfz  10178  fzolb2  10319  elfzo3  10328  fzouzsplit  10345  bitsval2  12421  rpexp  12641  isghm3  13747  isabl2  13797  dfrhm2  14083  bastop1  14722  cnntr  14864  lmres  14887  tx1cn  14908  tx2cn  14909  xmetec  15076  lgsabs1  15683