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 222	1 ⊢ (𝜒 → (𝜑 ↔ 𝜓))

Syntax hints:   → wi 4   ↔ wb 205   ∧ 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 206  df-an 396

This theorem is referenced by:  pm5.75  1025  cador  1611  reusv1  5315  reusv2lem1  5316  fpwwe2  10330  fzsplit2  13210  saddisjlem  16099  smupval  16123  smueqlem  16125  prmrec  16551  ablnsg  19363  cnprest  22348  flimrest  23042  fclsrest  23083  tsmssubm  23202  setsxms  23540  tcphcph  24306  ellimc2  24946  fsumvma2  26267  chpub  26273  mdbr2  30559  mdsl2i  30585  fzsplit3  31017  posrasymb  31145  trleile  31151  fvineqsneu  35509  cnvcnvintabd  41097  grumnud  41793  mofeu  46063