Theorem rbaib 541

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

Syntax hints:   → wi 4   ↔ wb 208   ∧ wa 398

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 209  df-an 399

This theorem is referenced by:  pm5.75  1025  cador  1609  reusv1  5298  reusv2lem1  5299  fpwwe2  10065  fzsplit2  12933  saddisjlem  15813  smupval  15837  smueqlem  15839  prmrec  16258  ablnsg  18967  cnprest  21897  flimrest  22591  fclsrest  22632  tsmssubm  22751  setsxms  23089  tcphcph  23840  ellimc2  24475  fsumvma2  25790  chpub  25796  mdbr2  30073  mdsl2i  30099  fzsplit3  30517  posrasymb  30644  trleile  30653  fvineqsneu  34695  cnvcnvintabd  39980  grumnud  40642