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

Theorem exancom 1864
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 1850 1 (∃𝑥(𝜑𝜓) ↔ ∃𝑥(𝜓𝜑))
Colors of variables: wff setvar class
Syntax hints:  wb 205  wa 396  wex 1781
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811
This theorem depends on definitions:  df-bi 206  df-an 397  df-ex 1782
This theorem is referenced by:  19.42v  1957  19.42  2229  eupickb  2635  datisi  2679  disamis  2680  dimatis  2687  fresison  2688  bamalip  2691  risset  3220  morex  3676  pwpw0  4772  pwsnOLD  4857  dfuni2  4866  eluni2  4868  uniprOLD  4883  dfiun2gOLD  4990  cnvco  5840  imadif  6583  uniuni  7693  pceu  16715  gsumval3eu  19677  isch3  30081  tgoldbachgt  33167  bnj1109  33289  bnj1304  33322  bnj849  33428  funpartlem  34516  bj-19.41t  35228  bj-elsngl  35428  bj-ccinftydisj  35673  mopickr  36813  moantr  36814  brcosscnvcoss  36885  rr-groth  42559  rr-grothshortbi  42563  eluni2f  43293  ssfiunibd  43517  setrec1lem3  47104
  Copyright terms: Public domain W3C validator