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  2239  eupickb  2630  datisi  2675  disamis  2676  dimatis  2683  fresison  2684  bamalip  2687  risset  3207  morex  3673  pwpw0  4762  dfuni2  4858  eluni2  4860  cnvco  5824  imadif  6565  uniuni  7695  pceu  16758  gsumval3eu  19816  isch3  31221  tgoldbachgt  34676  bnj1109  34798  bnj1304  34831  bnj849  34937  onvf1odlem1  35147  funpartlem  35986  bj-19.41t  36818  bj-elsngl  37012  bj-ccinftydisj  37257  mopickr  38405  moantr  38406  brcosscnvcoss  38546  rr-groth  44402  rr-grothshortbi  44406  eluni2f  45210  ssfiunibd  45420  chnsubseqword  46986  setrec1lem3  49800