Theorem exancom 1891

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 465	. 2 ⊢ ((𝜑 ∧ 𝜓) ↔ (𝜓 ∧ 𝜑))
2	1	exbii 1878	1 ⊢ (∃𝑥(𝜑 ∧ 𝜓) ↔ ∃𝑥(𝜓 ∧ 𝜑))

Syntax hints:   ↔ wb 209   ∧ wa 400  ∃wex 1809

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1825  ax-4 1839

This theorem depends on definitions:  df-bi 210  df-an 401  df-ex 1810

This theorem is referenced by:  19.42v  1983  19.42  2272  eupickb  2663  datisi  2707  disamis  2708  dimatis  2715  fresison  2716  bamalip  2719  risset  3240  morex  3682  pwpw0  4779  dfuni2  4874  eluni2  4876  cnvco  5875  imadif  6620  uniuni  7757  pceu  16901  gsumval3eu  19969  isch3  31593  tgoldbachgt  35050  bnj1109  35175  bnj1304  35207  bnj849  35313  onvf1odlem1  35587  funpartlem  36434  bj-19.41t  37411  bj-elsngl  37624  bj-ccinftydisj  37877  mopickr  39040  moantr  39041  brcosscnvcoss  39193  rr-groth  45029  rr-grothshortbi  45033  eluni2f  45841  ssfiunibd  46048  chnsubseqword  47614  setrec1lem3  50487