Theorem exancom 1863

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 1850	1 ⊢ (∃𝑥(𝜑 ∧ 𝜓) ↔ ∃𝑥(𝜓 ∧ 𝜑))

Syntax hints:   ↔ wb 206   ∧ wa 395  ∃wex 1781

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

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1782

This theorem is referenced by:  19.42v  1955  19.42  2244  eupickb  2635  datisi  2680  disamis  2681  dimatis  2688  fresison  2689  bamalip  2692  risset  3212  morex  3665  pwpw0  4756  dfuni2  4852  eluni2  4854  cnvco  5840  imadif  6582  uniuni  7716  pceu  16817  gsumval3eu  19879  isch3  31312  tgoldbachgt  34807  bnj1109  34929  bnj1304  34961  bnj849  35067  onvf1odlem1  35285  funpartlem  36124  bj-19.41t  37063  bj-elsngl  37275  bj-ccinftydisj  37527  mopickr  38692  moantr  38693  brcosscnvcoss  38845  rr-groth  44726  rr-grothshortbi  44730  eluni2f  45533  ssfiunibd  45742  chnsubseqword  47308  setrec1lem3  50164