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  1609  reusv1  5337  reusv2lem1  5338  fpwwe2  10541  fzsplit2  13451  saddisjlem  16377  smupval  16401  smueqlem  16403  prmrec  16836  ablnsg  19761  cnprest  23205  flimrest  23899  fclsrest  23940  tsmssubm  24059  setsxms  24395  tcphcph  25165  ellimc2  25806  fsumvma2  27153  chpub  27159  mdbr2  32278  mdsl2i  32304  fzsplit3  32780  posrasymb  32955  trleile  32959  fvineqsneu  37476  cnvcnvintabd  43717  grumnud  44403  mofeu  48972