Theorem rbaib 539

Description: Move conjunction outside of biconditional. (Contributed by Mario Carneiro, 11-Sep-2015.) (Proof shortened by Wolf Lammen, 19-Jan-2020.)

Hypothesis

Ref	Expression
baib.1	⊢ (𝜑 ↔ (𝜓 ∧ 𝜒))

Assertion

Ref	Expression
rbaib	⊢ (𝜒 → (𝜑 ↔ 𝜓))

Proof of Theorem rbaib

Step	Hyp	Ref	Expression
1		baib.1	. . 3 ⊢ (𝜑 ↔ (𝜓 ∧ 𝜒))
2	1	rbaibr 538	. 2 ⊢ (𝜒 → (𝜓 ↔ 𝜑))
3	2	bicomd 222	1 ⊢ (𝜒 → (𝜑 ↔ 𝜓))

Syntax hints:   → wi 4   ↔ wb 205   ∧ wa 396

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This theorem depends on definitions:  df-bi 206  df-an 397

This theorem is referenced by:  pm5.75  1027  cador  1609  reusv1  5357  reusv2lem1  5358  fpwwe2  10588  fzsplit2  13476  saddisjlem  16355  smupval  16379  smueqlem  16381  prmrec  16805  ablnsg  19639  cnprest  22677  flimrest  23371  fclsrest  23412  tsmssubm  23531  setsxms  23871  tcphcph  24638  ellimc2  25278  fsumvma2  26599  chpub  26605  mdbr2  31301  mdsl2i  31327  fzsplit3  31765  posrasymb  31895  trleile  31901  fvineqsneu  35955  cnvcnvintabd  41994  grumnud  42688  mofeu  47034