Theorem exancom 1860

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

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

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

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

This theorem is referenced by:  19.42v  1953  19.42  2237  eupickb  2638  datisi  2683  disamis  2684  dimatis  2691  fresison  2692  bamalip  2695  risset  3239  morex  3741  pwpw0  4838  dfuni2  4933  eluni2  4935  dfiun2gOLD  5054  cnvco  5910  imadif  6662  uniuni  7797  pceu  16893  gsumval3eu  19946  isch3  31273  tgoldbachgt  34640  bnj1109  34762  bnj1304  34795  bnj849  34901  funpartlem  35906  bj-19.41t  36740  bj-elsngl  36934  bj-ccinftydisj  37179  mopickr  38319  moantr  38320  brcosscnvcoss  38390  rr-groth  44268  rr-grothshortbi  44272  eluni2f  45005  ssfiunibd  45224  setrec1lem3  48781