Theorem rbaib 543

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

Syntax hints:   → wi 4   ↔ wb 207   ∧ 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 208  df-an 397

This theorem is referenced by:  pm5.75  1036  cador  1615  reusv1  5333  reusv2lem1  5334  fpwwe2  10564  fzsplit2  13501  saddisjlem  16431  smupval  16455  smueqlem  16457  prmrec  16891  ablnsg  19820  cnprest  23279  flimrest  23973  fclsrest  24014  tsmssubm  24133  setsxms  24469  tcphcph  25229  ellimc2  25869  fsumvma2  27202  chpub  27208  mdbr2  32392  mdsl2i  32418  fzsplit3  32892  posrasymb  33053  trleile  33057  fvineqsneu  37780  cnvcnvintabd  44051  grumnud  44737  mofeu  49345