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  1031  cador  1610  reusv1  5339  reusv2lem1  5340  fpwwe2  10566  fzsplit2  13503  saddisjlem  16433  smupval  16457  smueqlem  16459  prmrec  16893  ablnsg  19822  cnprest  23254  flimrest  23948  fclsrest  23989  tsmssubm  24108  setsxms  24444  tcphcph  25204  ellimc2  25844  fsumvma2  27177  chpub  27183  mdbr2  32367  mdsl2i  32393  fzsplit3  32866  posrasymb  33027  trleile  33031  fvineqsneu  37727  cnvcnvintabd  44027  grumnud  44713  mofeu  49323