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  2275  eupickb  2665  datisi  2709  disamis  2710  dimatis  2717  fresison  2718  bamalip  2721  risset  3242  morex  3684  pwpw0  4781  dfuni2  4876  eluni2  4878  cnvco  5877  imadif  6624  uniuni  7767  pceu  16930  gsumval3eu  20020  isch3  31666  tgoldbachgt  35117  bnj1109  35242  bnj1304  35274  bnj849  35380  onvf1odlem1  35646  funpartlem  36473  bj-19.41t  37450  bj-elsngl  37663  bj-ccinftydisj  37916  mopickr  39080  moantr  39081  brcosscnvcoss  39233  rr-groth  45069  rr-grothshortbi  45073  eluni2f  45881  ssfiunibd  46088  chnsubseqword  47654  setrec1lem3  50526