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  1044  cador  1631  reusv1  5358  reusv2lem1  5359  fpwwe2  10616  fzsplit2  13565  saddisjlem  16510  smupval  16534  smueqlem  16536  prmrec  16970  ablnsg  19905  cnprest  23403  flimrest  24097  fclsrest  24138  tsmssubm  24257  setsxms  24593  tcphcph  25353  ellimc2  25993  fsumvma2  27332  chpub  27338  mdbr2  32553  mdsl2i  32579  fzsplit3  33046  posrasymb  33195  trleile  33199  fvineqsneu  37912  cnvcnvintabd  44183  grumnud  44855  mofeu  49478