Theorem exancom 1862

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

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

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

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

This theorem is referenced by:  19.42v  1954  19.42  2241  eupickb  2633  datisi  2678  disamis  2679  dimatis  2686  fresison  2687  bamalip  2690  risset  3209  morex  3675  pwpw0  4767  dfuni2  4863  eluni2  4865  cnvco  5832  imadif  6574  uniuni  7705  pceu  16772  gsumval3eu  19831  isch3  31265  tgoldbachgt  34769  bnj1109  34891  bnj1304  34924  bnj849  35030  onvf1odlem1  35246  funpartlem  36085  bj-19.41t  36918  bj-elsngl  37112  bj-ccinftydisj  37357  mopickr  38495  moantr  38496  brcosscnvcoss  38636  rr-groth  44482  rr-grothshortbi  44486  eluni2f  45289  ssfiunibd  45499  chnsubseqword  47064  setrec1lem3  49876