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  2273  eupickb  2661  datisi  2705  disamis  2706  dimatis  2713  fresison  2714  bamalip  2717  risset  3238  morex  3677  pwpw0  4774  dfuni2  4869  eluni2  4871  cnvco  5867  imadif  6624  uniuni  7776  setrec1lem3  9969  pceu  17024  gsumval3eu  20118  isch3  31843  tgoldbachgt  35292  bnj1109  35417  bnj1304  35449  bnj849  35555  onvf1odlem1  35882  funpartlem  36706  bj-19.41t  37668  bj-elsngl  37881  bj-ccinftydisj  38134  mopickr  39303  moantr  39304  brcosscnvcoss  39456  rr-groth  45282  rr-grothshortbi  45286  eluni2f  46117  ssfiunibd  46324