Theorem exancom 1865

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

Syntax hints:   ↔ wb 205   ∧ wa 395  ∃wex 1783

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

This theorem depends on definitions:  df-bi 206  df-an 396  df-ex 1784

This theorem is referenced by:  19.42v  1958  19.42  2232  eupickb  2637  datisi  2681  disamis  2682  dimatis  2689  fresison  2690  bamalip  2693  risset  3193  morex  3649  pwpw0  4743  pwsnOLD  4829  dfuni2  4838  eluni2  4840  uniprOLD  4855  dfiun2g  4957  cnvco  5783  imadif  6502  uniuni  7590  pceu  16475  gsumval3eu  19420  isch3  29504  tgoldbachgt  32543  bnj1109  32666  bnj1304  32699  bnj849  32805  funpartlem  34171  bj-19.41t  34883  bj-elsngl  35085  bj-ccinftydisj  35311  moantr  36421  brcosscnvcoss  36484  rr-groth  41806  rr-grothshortbi  41810  eluni2f  42542  ssfiunibd  42738  setrec1lem3  46281