Theorem rbaib 546

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 545	. 2 ⊢ (𝜒 → (𝜓 ↔ 𝜑))
3	2	bicomd 225	1 ⊢ (𝜒 → (𝜑 ↔ 𝜓))

Syntax hints:   → wi 4   ↔ wb 208   ∧ wa 399

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 209  df-an 400

This theorem is referenced by:  pm5.75  1041  cador  1627  reusv1  5353  reusv2lem1  5354  fpwwe2  10598  fzsplit2  13551  saddisjlem  16481  smupval  16505  smueqlem  16507  prmrec  16941  ablnsg  19870  cnprest  23329  flimrest  24023  fclsrest  24064  tsmssubm  24183  setsxms  24519  tcphcph  25279  ellimc2  25919  fsumvma2  27255  chpub  27261  mdbr2  32445  mdsl2i  32471  fzsplit3  32945  posrasymb  33106  trleile  33110  fvineqsneu  37869  cnvcnvintabd  44140  grumnud  44826  mofeu  49433