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  1608  reusv1  5352  reusv2lem1  5353  fpwwe2  10596  fzsplit2  13510  saddisjlem  16434  smupval  16458  smueqlem  16460  prmrec  16893  ablnsg  19777  cnprest  23176  flimrest  23870  fclsrest  23911  tsmssubm  24030  setsxms  24367  tcphcph  25137  ellimc2  25778  fsumvma2  27125  chpub  27131  mdbr2  32225  mdsl2i  32251  fzsplit3  32716  posrasymb  32891  trleile  32897  fvineqsneu  37399  cnvcnvintabd  43589  grumnud  44275  mofeu  48836