Theorem exancom 1857

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

Syntax hints:   ↔ wb 205   ∧ wa 395  ∃wex 1774

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

This theorem depends on definitions:  df-bi 206  df-an 396  df-ex 1775

This theorem is referenced by:  19.42v  1950  19.42  2225  eupickb  2627  datisi  2671  disamis  2672  dimatis  2679  fresison  2680  bamalip  2683  risset  3227  morex  3714  pwpw0  4817  dfuni2  4910  eluni2  4912  uniprOLD  4926  dfiun2gOLD  5034  cnvco  5888  imadif  6637  uniuni  7764  pceu  16814  gsumval3eu  19858  isch3  31050  tgoldbachgt  34295  bnj1109  34417  bnj1304  34450  bnj849  34556  funpartlem  35538  bj-19.41t  36251  bj-elsngl  36447  bj-ccinftydisj  36692  mopickr  37835  moantr  37836  brcosscnvcoss  37906  rr-groth  43736  rr-grothshortbi  43740  eluni2f  44469  ssfiunibd  44691  setrec1lem3  48120