Theorem exancom 1840

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

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

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

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

This theorem is referenced by:  19.42v  1929  19.42  2201  eupickb  2688  datisi  2737  disamis  2738  dimatis  2745  fresison  2746  bamalip  2749  risset  3228  morex  3641  pwpw0  4647  pwsnALT  4732  dfuni2  4741  eluni2  4743  unipr  4752  dfiun2g  4852  dfiun2gOLD  4853  cnvco  5634  imadif  6300  uniuni  7332  pceu  16000  gsumval3eu  18733  isch3  28697  tgoldbachgt  31507  bnj1109  31631  bnj1304  31664  bnj849  31769  funpartlem  32957  bj-elsngl  33831  bj-ccinftydisj  33999  moantr  35098  brcosscnvcoss  35160  rr-groth  40084  eluni2f  40862  ssfiunibd  41070  setrec1lem3  44226