Theorem exancom 1861

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 1848	1 ⊢ (∃𝑥(𝜑 ∧ 𝜓) ↔ ∃𝑥(𝜓 ∧ 𝜑))

Syntax hints:   ↔ wb 206   ∧ wa 395  ∃wex 1779

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

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1780

This theorem is referenced by:  19.42v  1953  19.42  2237  eupickb  2628  datisi  2673  disamis  2674  dimatis  2681  fresison  2682  bamalip  2685  risset  3204  morex  3679  pwpw0  4764  dfuni2  4860  eluni2  4862  cnvco  5828  imadif  6566  uniuni  7698  pceu  16758  gsumval3eu  19783  isch3  31185  tgoldbachgt  34637  bnj1109  34759  bnj1304  34792  bnj849  34898  onvf1odlem1  35086  funpartlem  35926  bj-19.41t  36758  bj-elsngl  36952  bj-ccinftydisj  37197  mopickr  38341  moantr  38342  brcosscnvcoss  38421  rr-groth  44282  rr-grothshortbi  44286  eluni2f  45091  ssfiunibd  45301  setrec1lem3  49684