Theorem rbaib 547

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 546	. 2 ⊢ (𝜒 → (𝜓 ↔ 𝜑))
3	2	bicomd 226	1 ⊢ (𝜒 → (𝜑 ↔ 𝜓))

Syntax hints:   → wi 4   ↔ wb 209   ∧ wa 400

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 210  df-an 401

This theorem is referenced by:  pm5.75  1046  cador  1638  reusv1  5370  reusv2lem1  5371  fpwwe2  10629  fzsplit2  13579  saddisjlem  16523  smupval  16547  smueqlem  16549  prmrec  16983  ablnsg  19918  cnprest  23427  flimrest  24121  fclsrest  24162  tsmssubm  24281  setsxms  24617  tcphcph  25377  ellimc2  26017  fsumvma2  27359  chpub  27365  mdbr2  32629  mdsl2i  32655  fzsplit3  33119  posrasymb  33268  trleile  33272  fvineqsneu  38038  cnvcnvintabd  44309  grumnud  44979  mofeu  49609  n0als  50577