Theorem exancom 1861

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

Syntax hints:   ↔ wb 208   ∧ wa 398  ∃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 209  df-an 399  df-ex 1781

This theorem is referenced by:  19.42v  1954  19.42  2238  eupickb  2720  datisi  2765  disamis  2766  dimatis  2773  fresison  2774  bamalip  2777  risset  3267  morex  3710  pwpw0  4746  pwsnOLD  4831  dfuni2  4840  eluni2  4842  unipr  4855  dfiun2g  4955  dfiun2gOLD  4956  cnvco  5756  imadif  6438  uniuni  7484  pceu  16183  gsumval3eu  19024  isch3  29018  tgoldbachgt  31934  bnj1109  32058  bnj1304  32091  bnj849  32197  funpartlem  33403  bj-19.41t  34103  bj-elsngl  34283  bj-ccinftydisj  34498  moantr  35631  brcosscnvcoss  35694  rr-groth  40655  eluni2f  41389  ssfiunibd  41596  setrec1lem3  44812