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

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

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

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

This theorem is referenced by:  19.42v  1953  19.42  2237  eupickb  2629  datisi  2674  disamis  2675  dimatis  2682  fresison  2683  bamalip  2686  risset  3213  morex  3693  pwpw0  4780  dfuni2  4876  eluni2  4878  dfiun2gOLD  4998  cnvco  5852  imadif  6603  uniuni  7741  pceu  16824  gsumval3eu  19841  isch3  31177  tgoldbachgt  34661  bnj1109  34783  bnj1304  34816  bnj849  34922  onvf1odlem1  35097  funpartlem  35937  bj-19.41t  36769  bj-elsngl  36963  bj-ccinftydisj  37208  mopickr  38352  moantr  38353  brcosscnvcoss  38432  rr-groth  44295  rr-grothshortbi  44299  eluni2f  45104  ssfiunibd  45314  setrec1lem3  49682