Theorem exancom 1864

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

Syntax hints:   ↔ wb 205   ∧ wa 396  ∃wex 1781

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

This theorem depends on definitions:  df-bi 206  df-an 397  df-ex 1782

This theorem is referenced by:  19.42v  1957  19.42  2229  eupickb  2631  datisi  2675  disamis  2676  dimatis  2683  fresison  2684  bamalip  2687  risset  3230  morex  3715  pwpw0  4816  pwsnOLD  4901  dfuni2  4910  eluni2  4912  uniprOLD  4927  dfiun2gOLD  5034  cnvco  5885  imadif  6632  uniuni  7748  pceu  16778  gsumval3eu  19771  isch3  30489  tgoldbachgt  33670  bnj1109  33792  bnj1304  33825  bnj849  33931  funpartlem  34909  bj-19.41t  35647  bj-elsngl  35844  bj-ccinftydisj  36089  mopickr  37227  moantr  37228  brcosscnvcoss  37299  rr-groth  43048  rr-grothshortbi  43052  eluni2f  43782  ssfiunibd  44009  setrec1lem3  47724