Theorem exancom 1865

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 462	. 2 ⊢ ((𝜑 ∧ 𝜓) ↔ (𝜓 ∧ 𝜑))
2	1	exbii 1851	1 ⊢ (∃𝑥(𝜑 ∧ 𝜓) ↔ ∃𝑥(𝜓 ∧ 𝜑))

Syntax hints:   ↔ wb 205   ∧ wa 397  ∃wex 1782

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

This theorem depends on definitions:  df-bi 206  df-an 398  df-ex 1783

This theorem is referenced by:  19.42v  1958  19.42  2230  eupickb  2632  datisi  2676  disamis  2677  dimatis  2684  fresison  2685  bamalip  2688  risset  3231  morex  3716  pwpw0  4817  pwsnOLD  4902  dfuni2  4911  eluni2  4913  uniprOLD  4928  dfiun2gOLD  5035  cnvco  5886  imadif  6633  uniuni  7749  pceu  16779  gsumval3eu  19772  isch3  30494  tgoldbachgt  33675  bnj1109  33797  bnj1304  33830  bnj849  33936  funpartlem  34914  bj-19.41t  35652  bj-elsngl  35849  bj-ccinftydisj  36094  mopickr  37232  moantr  37233  brcosscnvcoss  37304  rr-groth  43058  rr-grothshortbi  43062  eluni2f  43792  ssfiunibd  44019  setrec1lem3  47734