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  2635  datisi  2680  disamis  2681  dimatis  2688  fresison  2689  bamalip  2692  risset  3221  morex  3707  pwpw0  4794  dfuni2  4890  eluni2  4892  dfiun2gOLD  5012  cnvco  5870  imadif  6625  uniuni  7761  pceu  16871  gsumval3eu  19890  isch3  31227  tgoldbachgt  34700  bnj1109  34822  bnj1304  34855  bnj849  34961  funpartlem  35965  bj-19.41t  36797  bj-elsngl  36991  bj-ccinftydisj  37236  mopickr  38386  moantr  38387  brcosscnvcoss  38457  rr-groth  44290  rr-grothshortbi  44294  eluni2f  45094  ssfiunibd  45305  setrec1lem3  49520