Metamath Proof Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >  exancom Structured version   Visualization version   GIF version

Theorem exancom 1900
 Description: Commutation of conjunction inside an existential quantifier. (Contributed by NM, 18-Aug-1993.)
Assertion
Ref Expression
exancom (∃𝑥(𝜑𝜓) ↔ ∃𝑥(𝜓𝜑))

Proof of Theorem exancom
StepHypRef Expression
1 ancom 465 . 2 ((𝜑𝜓) ↔ (𝜓𝜑))
21exbii 1887 1 (∃𝑥(𝜑𝜓) ↔ ∃𝑥(𝜓𝜑))
 Colors of variables: wff setvar class Syntax hints:   ↔ wb 196   ∧ wa 383  ∃wex 1817 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1835  ax-4 1850 This theorem depends on definitions:  df-bi 197  df-an 385  df-ex 1818 This theorem is referenced by:  19.42v  1994  19.42  2216  eupickb  2640  risset  3164  morex  3496  pwpw0  4452  pwsnALT  4537  dfuni2  4546  eluni2  4548  unipr  4557  dfiun2g  4660  cnvco  5415  imadif  6086  uniuni  7088  pceu  15674  gsumval3eu  18426  isch3  28328  tgoldbachgt  30971  bnj1109  31085  bnj1304  31118  bnj849  31223  funpartlem  32276  bj-elsngl  33183  bj-ccinftydisj  33332  moantr  34369  brcosscnvcoss  34431  eluni2f  39702  ssfiunibd  39939  setrec1lem3  42863
 Copyright terms: Public domain W3C validator