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  1026  cador  1610  reusv1  5320  reusv2lem1  5321  fpwwe2  10399  fzsplit2  13281  saddisjlem  16171  smupval  16195  smueqlem  16197  prmrec  16623  ablnsg  19448  cnprest  22440  flimrest  23134  fclsrest  23175  tsmssubm  23294  setsxms  23634  tcphcph  24401  ellimc2  25041  fsumvma2  26362  chpub  26368  mdbr2  30658  mdsl2i  30684  fzsplit3  31115  posrasymb  31243  trleile  31249  fvineqsneu  35582  cnvcnvintabd  41208  grumnud  41904  mofeu  46175