Theorem exancom 1893

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

This proof depends on syntax axioms:   ↔ wb 209   ∧ wa 401  ∃wex 1811

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841

This proof depends on definitions:  df-bi 210  df-an 402  df-ex 1812

This theorem is used by:  19.42v  1987  19.42  2275  eupickb  2663  datisi  2707  disamis  2708  dimatis  2715  fresison  2716  bamalip  2719  risset  3240  morex  3679  pwpw0  4833  dfuni2  4871  eluni2  4873  cnvco  5871  imadif  6632  uniuni  7783  setrec1lem3  9979  pceu  17036  gsumval3eu  20130  isch3  31855  tgoldbachgt  35345  bnj1109  35470  bnj1304  35502  bnj849  35608  onvf1odlem1  35985  funpartlem  36833  bj-19.41t  37795  bj-elsngl  38008  bj-ccinftydisj  38274  mopickr  39443  moantr  39444  brcosscnvcoss  39596  rr-groth  45423  rr-grothshortbi  45427  eluni2f  46257  ssfiunibd  46464