Theorem exancom 1861

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

Syntax hints:   ↔ wb 206   ∧ wa 395  ∃wex 1779

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

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1780

This theorem is referenced by:  19.42v  1953  19.42  2237  eupickb  2628  datisi  2673  disamis  2674  dimatis  2681  fresison  2682  bamalip  2685  risset  3212  morex  3690  pwpw0  4777  dfuni2  4873  eluni2  4875  dfiun2gOLD  4995  cnvco  5849  imadif  6600  uniuni  7738  pceu  16817  gsumval3eu  19834  isch3  31170  tgoldbachgt  34654  bnj1109  34776  bnj1304  34809  bnj849  34915  onvf1odlem1  35090  funpartlem  35930  bj-19.41t  36762  bj-elsngl  36956  bj-ccinftydisj  37201  mopickr  38345  moantr  38346  brcosscnvcoss  38425  rr-groth  44288  rr-grothshortbi  44292  eluni2f  45097  ssfiunibd  45307  setrec1lem3  49678