Theorem exancom 1894

Description: Commutation of conjunction inside an existential quantifier. (Contributed by NM, 18-Aug-1993.)

Assertion

Ref	Expression
exancom	⊢ (∃𝑥(𝜑 ∧ 𝜓) ↔ ∃𝑥(𝜓 ∧ 𝜑))

Proof of Theorem exancom

Step	Hyp	Ref	Expression
1		ancom 466	. 2 ⊢ ((𝜑 ∧ 𝜓) ↔ (𝜓 ∧ 𝜑))
2	1	exbii 1881	1 ⊢ (∃𝑥(𝜑 ∧ 𝜓) ↔ ∃𝑥(𝜓 ∧ 𝜑))

This proof depends on syntax axioms:   ↔ wb 209   ∧ wa 401  ∃wex 1812

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

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

This theorem is used by:  19.42v  1986  19.42  2272  eupickb  2660  datisi  2704  disamis  2705  dimatis  2712  fresison  2713  bamalip  2716  risset  3237  morex  3677  pwpw0  4774  dfuni2  4869  eluni2  4871  cnvco  5869  imadif  6618  uniuni  7762  pceu  16939  gsumval3eu  20032  isch3  31723  tgoldbachgt  35172  bnj1109  35297  bnj1304  35329  bnj849  35435  onvf1odlem1  35701  funpartlem  36522  bj-19.41t  37500  bj-elsngl  37713  bj-ccinftydisj  37966  mopickr  39120  moantr  39121  brcosscnvcoss  39273  rr-groth  45124  rr-grothshortbi  45128  eluni2f  45936  ssfiunibd  46143  setrec1lem3  50616