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  1027  cador  1609  reusv1  5344  reusv2lem1  5345  fpwwe2  10504  fzsplit2  13386  saddisjlem  16270  smupval  16294  smueqlem  16296  prmrec  16720  ablnsg  19543  cnprest  22545  flimrest  23239  fclsrest  23280  tsmssubm  23399  setsxms  23739  tcphcph  24506  ellimc2  25146  fsumvma2  26467  chpub  26473  mdbr2  30945  mdsl2i  30971  fzsplit3  31400  posrasymb  31528  trleile  31534  fvineqsneu  35736  cnvcnvintabd  41581  grumnud  42277  mofeu  46593