Theorem exancom 1869

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

Syntax hints:   ↔ wb 209   ∧ wa 399  ∃wex 1787

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

This theorem depends on definitions:  df-bi 210  df-an 400  df-ex 1788

This theorem is referenced by:  19.42v  1962  19.42  2236  eupickb  2636  datisi  2680  disamis  2681  dimatis  2688  fresison  2689  bamalip  2692  risset  3176  morex  3621  pwpw0  4712  pwsnOLD  4798  dfuni2  4807  eluni2  4809  uniprOLD  4824  dfiun2g  4926  cnvco  5739  imadif  6442  uniuni  7525  pceu  16362  gsumval3eu  19243  isch3  29276  tgoldbachgt  32309  bnj1109  32433  bnj1304  32466  bnj849  32572  funpartlem  33930  bj-19.41t  34642  bj-elsngl  34844  bj-ccinftydisj  35068  moantr  36180  brcosscnvcoss  36243  rr-groth  41531  rr-grothshortbi  41535  eluni2f  42267  ssfiunibd  42462  setrec1lem3  46009