Theorem rbaib 538

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

Syntax hints:   → wi 4   ↔ wb 206   ∧ wa 395

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 207  df-an 396

This theorem is referenced by:  pm5.75  1030  cador  1609  reusv1  5342  reusv2lem1  5343  fpwwe2  10554  fzsplit2  13465  saddisjlem  16391  smupval  16415  smueqlem  16417  prmrec  16850  ablnsg  19776  cnprest  23233  flimrest  23927  fclsrest  23968  tsmssubm  24087  setsxms  24423  tcphcph  25193  ellimc2  25834  fsumvma2  27181  chpub  27187  mdbr2  32371  mdsl2i  32397  fzsplit3  32873  posrasymb  33049  trleile  33053  fvineqsneu  37612  cnvcnvintabd  43837  grumnud  44523  mofeu  49089