Theorem exancom 1774

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

Syntax hints:   ↔ wb 195   ∧ wa 383  ∃wex 1695

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

This theorem depends on definitions:  df-bi 196  df-an 385  df-ex 1696

This theorem is referenced by:  19.29rOLD  1791  19.42v  1905  19.42  2092  eupickb  2526  risset  3044  morex  3357  pwpw0  4284  pwsnALT  4367  dfuni2  4374  eluni2  4376  unipr  4385  dfiun2g  4488  cnvco  5230  imadif  5887  uniuni  6865  pceu  15389  gsumval3eu  18128  isch3  27482  bnj1109  30111  bnj1304  30144  bnj849  30249  funpartlem  31219  bj-elsngl  32149  bj-ccinftydisj  32277  eluni2f  38315  ssfiunibd  38464  setrec1lem3  42235