Theorem exancom 1881

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

Syntax hints:   ↔ wb 208   ∧ wa 399  ∃wex 1799

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

This theorem depends on definitions:  df-bi 209  df-an 400  df-ex 1800

This theorem is referenced by:  19.42v  1973  19.42  2271  eupickb  2662  datisi  2706  disamis  2707  dimatis  2714  fresison  2715  bamalip  2718  risset  3237  morex  3682  pwpw0  4771  dfuni2  4867  eluni2  4869  cnvco  5861  imadif  6605  uniuni  7745  pceu  16882  gsumval3eu  19944  isch3  31444  tgoldbachgt  34957  bnj1109  35082  bnj1304  35114  bnj849  35220  onvf1odlem1  35446  funpartlem  36292  bj-19.41t  37241  bj-elsngl  37453  bj-ccinftydisj  37705  mopickr  38870  moantr  38871  brcosscnvcoss  39023  rr-groth  44875  rr-grothshortbi  44879  eluni2f  45681  ssfiunibd  45888  chnsubseqword  47454  setrec1lem3  50310