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  5373  reusv2lem1  5374  fpwwe2  10646  fzsplit2  13596  saddisjlem  16547  smupval  16571  smueqlem  16573  prmrec  17007  ablnsg  19948  cnprest  23483  flimrest  24177  fclsrest  24218  tsmssubm  24337  setsxms  24673  tcphcph  25433  ellimc2  26073  fsumvma2  27415  chpub  27421  mdbr2  32685  mdsl2i  32711  fzsplit3  33175  posrasymb  33318  trleile  33322  fvineqsneu  38098  cnvcnvintabd  44367  grumnud  45037  mofeu  49667  n0als  50635