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  2243  eupickb  2635  datisi  2680  disamis  2681  dimatis  2688  fresison  2689  bamalip  2692  risset  3211  morex  3677  pwpw0  4769  dfuni2  4865  eluni2  4867  cnvco  5834  imadif  6576  uniuni  7707  pceu  16774  gsumval3eu  19833  isch3  31316  tgoldbachgt  34820  bnj1109  34942  bnj1304  34975  bnj849  35081  onvf1odlem1  35297  funpartlem  36136  bj-19.41t  36975  bj-elsngl  37169  bj-ccinftydisj  37418  mopickr  38566  moantr  38567  brcosscnvcoss  38707  rr-groth  44550  rr-grothshortbi  44554  eluni2f  45357  ssfiunibd  45567  chnsubseqword  47132  setrec1lem3  49944