Theorem exancom 1868

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

Syntax hints:   ↔ wb 207   ∧ wa 396  ∃wex 1786

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

This theorem depends on definitions:  df-bi 208  df-an 397  df-ex 1787

This theorem is referenced by:  19.42v  1960  19.42  2248  eupickb  2639  datisi  2683  disamis  2684  dimatis  2691  fresison  2692  bamalip  2695  risset  3214  morex  3660  pwpw0  4744  dfuni2  4840  eluni2  4842  cnvco  5827  imadif  6569  uniuni  7705  pceu  16808  gsumval3eu  19870  isch3  31330  tgoldbachgt  34847  bnj1109  34969  bnj1304  35001  bnj849  35107  onvf1odlem1  35331  funpartlem  36170  bj-19.41t  37109  bj-elsngl  37321  bj-ccinftydisj  37573  mopickr  38738  moantr  38739  brcosscnvcoss  38891  rr-groth  44743  rr-grothshortbi  44747  eluni2f  45550  ssfiunibd  45757  chnsubseqword  47323  setrec1lem3  50179