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

Theorem exancom 1938
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 448 . 2 ((𝜑𝜓) ↔ (𝜓𝜑))
21exbii 1924 1 (∃𝑥(𝜑𝜓) ↔ ∃𝑥(𝜓𝜑))
Colors of variables: wff setvar class
Syntax hints:  wb 196  wa 382  wex 1852
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1870  ax-4 1885
This theorem depends on definitions:  df-bi 197  df-an 383  df-ex 1853
This theorem is referenced by:  19.42v  2033  19.42  2261  eupickb  2687  risset  3210  morex  3542  pwpw0  4480  pwsnALT  4568  dfuni2  4577  eluni2  4579  unipr  4588  dfiun2g  4687  cnvco  5445  imadif  6112  uniuni  7121  pceu  15757  gsumval3eu  18511  isch3  28437  tgoldbachgt  31080  bnj1109  31194  bnj1304  31227  bnj849  31332  funpartlem  32385  bj-elsngl  33286  bj-ccinftydisj  33436  moantr  34468  brcosscnvcoss  34530  eluni2f  39807  ssfiunibd  40037  setrec1lem3  42961
  Copyright terms: Public domain W3C validator