Theorem rbaib 536

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

Syntax hints:   → wi 4   ↔ wb 198   ∧ wa 386

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 199  df-an 387

This theorem is referenced by:  cador  1723  reusv1  5096  reusv2lem1  5097  opelresgOLD2  5638  fpwwe2  9779  fzsplit2  12658  saddisjlem  15558  smupval  15582  smueqlem  15584  prmrec  15996  ablnsg  18602  cnprest  21463  flimrest  22156  fclsrest  22197  tsmssubm  22315  setsxms  22653  tcphcph  23404  ellimc2  24039  fsumvma2  25351  chpub  25357  mdbr2  29709  mdsl2i  29735  fzsplit3  30099  posrasymb  30201  trleile  30210  cnvcnvintabd  38746