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  1988  19.42  2276  eupickb  2663  datisi  2707  disamis  2708  dimatis  2715  fresison  2716  bamalip  2719  risset  3241  morex  3680  pwpw0  4836  dfuni2  4874  eluni2  4876  cnvco  5879  imadif  6654  uniuni  7808  setrec1lem3  10006  pceu  17068  gsumval3eu  20169  isch3  31900  tgoldbachgt  35403  bnj1109  35528  bnj1304  35560  bnj849  35666  onvf1odlem1  36072  funpartlem  36921  bj-19.41t  37883  bj-elsngl  38096  bj-ccinftydisj  38402  mopickr  39569  moantr  39570  brcosscnvcoss  39722  rr-groth  45544  rr-grothshortbi  45548  eluni2f  46391  ssfiunibd  46598