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  1030  cador  1608  reusv1  5355  reusv2lem1  5356  fpwwe2  10603  fzsplit2  13517  saddisjlem  16441  smupval  16465  smueqlem  16467  prmrec  16900  ablnsg  19784  cnprest  23183  flimrest  23877  fclsrest  23918  tsmssubm  24037  setsxms  24374  tcphcph  25144  ellimc2  25785  fsumvma2  27132  chpub  27138  mdbr2  32232  mdsl2i  32258  fzsplit3  32723  posrasymb  32898  trleile  32904  fvineqsneu  37406  cnvcnvintabd  43596  grumnud  44282  mofeu  48840