Theorem rbaib 548

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

This proof depends on syntax axioms:   → wi 4   ↔ wb 209   ∧ wa 401

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This proof depends on definitions:  df-bi 210  df-an 402

This theorem is used by:  pm5.75  1046  cador  1641  reusv1  5364  reusv2lem1  5365  fpwwe2  10758  fzsplit2  13713  saddisjlem  16666  smupval  16690  smueqlem  16692  prmrec  17132  ablnsg  20094  cnprest  23640  flimrest  24335  fclsrest  24376  tsmssubm  24495  setsxms  24831  tcphcph  25591  ellimc2  26230  fsumvma2  27574  chpub  27580  mdbr2  32931  mdsl2i  32957  fzsplit3  33458  posrasymb  33601  trleile  33605  fvineqsneu  38539  cnvcnvintabd  44803  grumnud  45473  mofeu  50174  n0als  51224