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  3679  pwpw0  4771  dfuni2  4867  eluni2  4869  cnvco  5842  imadif  6584  uniuni  7717  pceu  16786  gsumval3eu  19845  isch3  31329  tgoldbachgt  34841  bnj1109  34963  bnj1304  34995  bnj849  35101  onvf1odlem1  35319  funpartlem  36158  bj-19.41t  37009  bj-elsngl  37216  bj-ccinftydisj  37468  mopickr  38622  moantr  38623  brcosscnvcoss  38775  rr-groth  44655  rr-grothshortbi  44659  eluni2f  45462  ssfiunibd  45671  chnsubseqword  47236  setrec1lem3  50048