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  34631  bnj1109  34753  bnj1304  34786  bnj849  34892  onvf1odlem1  35080  funpartlem  35920  bj-19.41t  36752  bj-elsngl  36946  bj-ccinftydisj  37191  mopickr  38335  moantr  38336  brcosscnvcoss  38415  rr-groth  44276  rr-grothshortbi  44280  eluni2f  45085  ssfiunibd  45295  setrec1lem3  49678