Theorem exancom 1859

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

Syntax hints:   ↔ wb 206   ∧ wa 395  ∃wex 1776

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

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1777

This theorem is referenced by:  19.42v  1951  19.42  2234  eupickb  2633  datisi  2678  disamis  2679  dimatis  2686  fresison  2687  bamalip  2690  risset  3231  morex  3728  pwpw0  4818  dfuni2  4914  eluni2  4916  dfiun2gOLD  5036  cnvco  5899  imadif  6652  uniuni  7781  pceu  16880  gsumval3eu  19937  isch3  31270  tgoldbachgt  34657  bnj1109  34779  bnj1304  34812  bnj849  34918  funpartlem  35924  bj-19.41t  36757  bj-elsngl  36951  bj-ccinftydisj  37196  mopickr  38345  moantr  38346  brcosscnvcoss  38416  rr-groth  44295  rr-grothshortbi  44299  eluni2f  45043  ssfiunibd  45260  setrec1lem3  48920