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  5344  reusv2lem1  5345  fpwwe2  10566  fzsplit2  13477  saddisjlem  16403  smupval  16427  smueqlem  16429  prmrec  16862  ablnsg  19788  cnprest  23245  flimrest  23939  fclsrest  23980  tsmssubm  24099  setsxms  24435  tcphcph  25205  ellimc2  25846  fsumvma2  27193  chpub  27199  mdbr2  32383  mdsl2i  32409  fzsplit3  32883  posrasymb  33059  trleile  33063  fvineqsneu  37660  cnvcnvintabd  43950  grumnud  44636  mofeu  49201