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  1029  cador  1605  reusv1  5415  reusv2lem1  5416  fpwwe2  10712  fzsplit2  13609  saddisjlem  16510  smupval  16534  smueqlem  16536  prmrec  16969  ablnsg  19889  cnprest  23318  flimrest  24012  fclsrest  24053  tsmssubm  24172  setsxms  24512  tcphcph  25290  ellimc2  25932  fsumvma2  27276  chpub  27282  mdbr2  32328  mdsl2i  32354  fzsplit3  32799  posrasymb  32938  trleile  32944  fvineqsneu  37377  cnvcnvintabd  43562  grumnud  44255  mofeu  48561