Theorem exancom 1888

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

Syntax hints:   ↔ wb 209   ∧ wa 400  ∃wex 1806

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

This theorem depends on definitions:  df-bi 210  df-an 401  df-ex 1807

This theorem is referenced by:  19.42v  1980  19.42  2278  eupickb  2669  datisi  2713  disamis  2714  dimatis  2721  fresison  2722  bamalip  2725  risset  3246  morex  3691  pwpw0  4783  dfuni2  4878  eluni2  4880  cnvco  5876  imadif  6621  uniuni  7761  pceu  16906  gsumval3eu  19974  isch3  31534  tgoldbachgt  34995  bnj1109  35120  bnj1304  35152  bnj849  35258  onvf1odlem1  35486  funpartlem  36333  bj-19.41t  37280  bj-elsngl  37492  bj-ccinftydisj  37745  mopickr  38910  moantr  38911  brcosscnvcoss  39063  rr-groth  44901  rr-grothshortbi  44905  eluni2f  45713  ssfiunibd  45920  chnsubseqword  47486  setrec1lem3  50352