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  2236  eupickb  2635  datisi  2680  disamis  2681  dimatis  2688  fresison  2689  bamalip  2692  risset  3233  morex  3725  pwpw0  4813  dfuni2  4909  eluni2  4911  dfiun2gOLD  5031  cnvco  5896  imadif  6650  uniuni  7782  pceu  16884  gsumval3eu  19922  isch3  31260  tgoldbachgt  34678  bnj1109  34800  bnj1304  34833  bnj849  34939  funpartlem  35943  bj-19.41t  36775  bj-elsngl  36969  bj-ccinftydisj  37214  mopickr  38364  moantr  38365  brcosscnvcoss  38435  rr-groth  44318  rr-grothshortbi  44322  eluni2f  45108  ssfiunibd  45321  setrec1lem3  49208