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  16941  gsumval3eu  20034  isch3  31725  tgoldbachgt  35174  bnj1109  35299  bnj1304  35331  bnj849  35437  onvf1odlem1  35703  funpartlem  36524  bj-19.41t  37502  bj-elsngl  37715  bj-ccinftydisj  37968  mopickr  39122  moantr  39123  brcosscnvcoss  39275  rr-groth  45126  rr-grothshortbi  45130  eluni2f  45938  ssfiunibd  46145  setrec1lem3  50618