Theorem rbaib 538

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

Syntax hints:   → wi 4   ↔ wb 206   ∧ wa 395

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 207  df-an 396

This theorem is referenced by:  pm5.75  1030  cador  1604  reusv1  5402  reusv2lem1  5403  fpwwe2  10680  fzsplit2  13585  saddisjlem  16497  smupval  16521  smueqlem  16523  prmrec  16955  ablnsg  19879  cnprest  23312  flimrest  24006  fclsrest  24047  tsmssubm  24166  setsxms  24506  tcphcph  25284  ellimc2  25926  fsumvma2  27272  chpub  27278  mdbr2  32324  mdsl2i  32350  fzsplit3  32801  posrasymb  32939  trleile  32945  fvineqsneu  37393  cnvcnvintabd  43589  grumnud  44281  mofeu  48677