Theorem exancom 1862

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

Syntax hints:   ↔ wb 205   ∧ wa 394  ∃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 206  df-an 395  df-ex 1780

This theorem is referenced by:  19.42v  1955  19.42  2227  eupickb  2629  datisi  2673  disamis  2674  dimatis  2681  fresison  2682  bamalip  2685  risset  3228  morex  3714  pwpw0  4815  pwsnOLD  4900  dfuni2  4909  eluni2  4911  uniprOLD  4926  dfiun2gOLD  5033  cnvco  5884  imadif  6631  uniuni  7751  pceu  16783  gsumval3eu  19813  isch3  30761  tgoldbachgt  33973  bnj1109  34095  bnj1304  34128  bnj849  34234  funpartlem  35218  bj-19.41t  35955  bj-elsngl  36152  bj-ccinftydisj  36397  mopickr  37535  moantr  37536  brcosscnvcoss  37607  rr-groth  43360  rr-grothshortbi  43364  eluni2f  44093  ssfiunibd  44317  setrec1lem3  47821