Theorem exancom 1864

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

Syntax hints:   ↔ wb 205   ∧ wa 396  ∃wex 1782

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

This theorem depends on definitions:  df-bi 206  df-an 397  df-ex 1783

This theorem is referenced by:  19.42v  1957  19.42  2229  eupickb  2637  datisi  2681  disamis  2682  dimatis  2689  fresison  2690  bamalip  2693  risset  3194  morex  3654  pwpw0  4746  pwsnOLD  4832  dfuni2  4841  eluni2  4843  uniprOLD  4858  dfiun2gOLD  4961  cnvco  5794  imadif  6518  uniuni  7612  pceu  16547  gsumval3eu  19505  isch3  29603  tgoldbachgt  32643  bnj1109  32766  bnj1304  32799  bnj849  32905  funpartlem  34244  bj-19.41t  34956  bj-elsngl  35158  bj-ccinftydisj  35384  moantr  36494  brcosscnvcoss  36557  rr-groth  41917  rr-grothshortbi  41921  eluni2f  42653  ssfiunibd  42848  setrec1lem3  46395