Theorem rbaib 947

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

Syntax hints:   → wi 4   ↔ wb 196   ∧ wa 384

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 197  df-an 386

This theorem is referenced by:  cador  1547  reusv1  4866  reusv1OLD  4867  reusv2lem1  4868  opres  5406  cores  5638  fvres  6207  fpwwe2  9465  fzsplit2  12366  saddisjlem  15186  smupval  15210  smueqlem  15212  prmrec  15626  ablnsg  18250  cnprest  21093  flimrest  21787  fclsrest  21828  tsmssubm  21946  setsxms  22284  tchcph  23036  ellimc2  23641  fsumvma2  24939  chpub  24945  mdbr2  29155  mdsl2i  29181  fzsplit3  29553  posrasymb  29657  trleile  29666  cnvcnvintabd  37906