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  5359  reusv2lem1  5360  fpwwe2  10709  fzsplit2  13663  saddisjlem  16614  smupval  16638  smueqlem  16640  prmrec  17080  ablnsg  20041  cnprest  23587  flimrest  24282  fclsrest  24323  tsmssubm  24442  setsxms  24778  tcphcph  25538  ellimc2  26177  fsumvma2  27523  chpub  27529  mdbr2  32880  mdsl2i  32906  fzsplit3  33367  posrasymb  33510  trleile  33514  fvineqsneu  38302  cnvcnvintabd  44559  grumnud  45229  mofeu  49902  n0als  50856