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

Theorem exancom 1947
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 450 . 2 ((𝜑𝜓) ↔ (𝜓𝜑))
21exbii 1933 1 (∃𝑥(𝜑𝜓) ↔ ∃𝑥(𝜓𝜑))
Colors of variables: wff setvar class
Syntax hints:  wb 197  wa 384  wex 1859
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1877  ax-4 1894
This theorem depends on definitions:  df-bi 198  df-an 385  df-ex 1860
This theorem is referenced by:  19.42v  2043  19.42  2272  eupickb  2699  datisi  2745  disamis  2747  dimatis  2756  fresison  2758  bamalip  2764  risset  3246  morex  3582  pwpw0  4528  pwsnALT  4616  dfuni2  4625  eluni2  4627  unipr  4636  dfiun2g  4737  cnvco  5503  imadif  6178  uniuni  7195  pceu  15762  gsumval3eu  18500  isch3  28420  tgoldbachgt  31060  bnj1109  31174  bnj1304  31207  bnj849  31312  funpartlem  32364  bj-elsngl  33260  bj-ccinftydisj  33411  moantr  34434  brcosscnvcoss  34496  eluni2f  39772  ssfiunibd  39998  setrec1lem3  42998
  Copyright terms: Public domain W3C validator