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

Theorem exancom 1862
 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 464 . 2 ((𝜑𝜓) ↔ (𝜓𝜑))
21exbii 1849 1 (∃𝑥(𝜑𝜓) ↔ ∃𝑥(𝜓𝜑))
 Colors of variables: wff setvar class Syntax hints:   ↔ wb 209   ∧ wa 399  ∃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 210  df-an 400  df-ex 1782 This theorem is referenced by:  19.42v  1954  19.42  2237  eupickb  2700  datisi  2745  disamis  2746  dimatis  2753  fresison  2754  bamalip  2757  risset  3229  morex  3661  pwpw0  4709  pwsnOLD  4796  dfuni2  4805  eluni2  4807  unipr  4820  dfiun2g  4920  dfiun2gOLD  4921  cnvco  5724  imadif  6412  uniuni  7468  pceu  16176  gsumval3eu  19020  isch3  29027  tgoldbachgt  32042  bnj1109  32166  bnj1304  32199  bnj849  32305  funpartlem  33511  bj-19.41t  34213  bj-elsngl  34399  bj-ccinftydisj  34623  moantr  35769  brcosscnvcoss  35832  rr-groth  40994  eluni2f  41726  ssfiunibd  41928  setrec1lem3  45206
 Copyright terms: Public domain W3C validator