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  2628  datisi  2673  disamis  2674  dimatis  2681  fresison  2682  bamalip  2685  risset  3210  morex  3687  pwpw0  4773  dfuni2  4869  eluni2  4871  cnvco  5839  imadif  6584  uniuni  7718  pceu  16793  gsumval3eu  19818  isch3  31220  tgoldbachgt  34647  bnj1109  34769  bnj1304  34802  bnj849  34908  onvf1odlem1  35083  funpartlem  35923  bj-19.41t  36755  bj-elsngl  36949  bj-ccinftydisj  37194  mopickr  38338  moantr  38339  brcosscnvcoss  38418  rr-groth  44281  rr-grothshortbi  44285  eluni2f  45090  ssfiunibd  45300  setrec1lem3  49671