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  5359  reusv2lem1  5360  fpwwe2  10616  fzsplit2  13568  saddisjlem  16512  smupval  16536  smueqlem  16538  prmrec  16972  ablnsg  19908  cnprest  23407  flimrest  24101  fclsrest  24142  tsmssubm  24261  setsxms  24597  tcphcph  25357  ellimc2  25997  fsumvma2  27336  chpub  27342  mdbr2  32557  mdsl2i  32583  fzsplit3  33050  posrasymb  33200  trleile  33204  fvineqsneu  37917  cnvcnvintabd  44188  grumnud  44860  mofeu  49477