Theorem rbaib 540

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

Syntax hints:   → wi 4   ↔ wb 205   ∧ wa 397

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 398

This theorem is referenced by:  pm5.75  1028  cador  1610  reusv1  5396  reusv2lem1  5397  fpwwe2  10638  fzsplit2  13526  saddisjlem  16405  smupval  16429  smueqlem  16431  prmrec  16855  ablnsg  19715  cnprest  22793  flimrest  23487  fclsrest  23528  tsmssubm  23647  setsxms  23987  tcphcph  24754  ellimc2  25394  fsumvma2  26717  chpub  26723  mdbr2  31549  mdsl2i  31575  fzsplit3  32005  posrasymb  32135  trleile  32141  fvineqsneu  36292  cnvcnvintabd  42351  grumnud  43045  mofeu  47514