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

Theorem exancom 1852
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 461 . 2 ((𝜑𝜓) ↔ (𝜓𝜑))
21exbii 1839 1 (∃𝑥(𝜑𝜓) ↔ ∃𝑥(𝜓𝜑))
Colors of variables: wff setvar class
Syntax hints:  wb 207  wa 396  wex 1771
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1787  ax-4 1801
This theorem depends on definitions:  df-bi 208  df-an 397  df-ex 1772
This theorem is referenced by:  19.42v  1945  19.42  2228  eupickb  2713  datisi  2760  disamis  2761  dimatis  2768  fresison  2769  bamalip  2772  risset  3264  morex  3707  pwpw0  4738  pwsnALT  4823  dfuni2  4832  eluni2  4834  unipr  4843  dfiun2g  4946  dfiun2gOLD  4947  cnvco  5749  imadif  6431  uniuni  7473  pceu  16171  gsumval3eu  18953  isch3  28945  tgoldbachgt  31833  bnj1109  31957  bnj1304  31990  bnj849  32096  funpartlem  33300  bj-19.41t  34000  bj-elsngl  34177  bj-ccinftydisj  34387  moantr  35497  brcosscnvcoss  35559  rr-groth  40512  eluni2f  41246  ssfiunibd  41452  setrec1lem3  44720
  Copyright terms: Public domain W3C validator