Theorem rbaib 534

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 533	. 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  1721  reusv1  5099  reusv2lem1  5100  opelresgOLD2  5643  fpwwe2  9787  fzsplit2  12666  saddisjlem  15566  smupval  15590  smueqlem  15592  prmrec  16004  ablnsg  18610  cnprest  21471  flimrest  22164  fclsrest  22205  tsmssubm  22323  setsxms  22661  tcphcph  23412  ellimc2  24047  fsumvma2  25359  chpub  25365  mdbr2  29706  mdsl2i  29732  fzsplit3  30096  posrasymb  30198  trleile  30207  cnvcnvintabd  38742