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  2636  datisi  2681  disamis  2682  dimatis  2689  fresison  2690  bamalip  2693  risset  3213  morex  3666  pwpw0  4757  dfuni2  4853  eluni2  4855  cnvco  5835  imadif  6577  uniuni  7710  pceu  16811  gsumval3eu  19873  isch3  31330  tgoldbachgt  34826  bnj1109  34948  bnj1304  34980  bnj849  35086  onvf1odlem1  35304  funpartlem  36143  bj-19.41t  37082  bj-elsngl  37294  bj-ccinftydisj  37546  mopickr  38709  moantr  38710  brcosscnvcoss  38862  rr-groth  44747  rr-grothshortbi  44751  eluni2f  45554  ssfiunibd  45763  chnsubseqword  47327  setrec1lem3  50179