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

Theorem exancom 1784
 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 466 . 2 ((𝜑𝜓) ↔ (𝜓𝜑))
21exbii 1771 1 (∃𝑥(𝜑𝜓) ↔ ∃𝑥(𝜓𝜑))
 Colors of variables: wff setvar class Syntax hints:   ↔ wb 196   ∧ wa 384  ∃wex 1701 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1719  ax-4 1734 This theorem depends on definitions:  df-bi 197  df-an 386  df-ex 1702 This theorem is referenced by:  19.42v  1915  19.42  2103  eupickb  2537  risset  3056  morex  3376  pwpw0  4317  pwsnALT  4402  dfuni2  4409  eluni2  4411  unipr  4420  dfiun2g  4523  cnvco  5273  imadif  5936  uniuni  6927  pceu  15486  gsumval3eu  18237  isch3  27968  bnj1109  30600  bnj1304  30633  bnj849  30738  funpartlem  31726  bj-elsngl  32638  bj-ccinftydisj  32768  eluni2f  38804  ssfiunibd  39018  setrec1lem3  41755
 Copyright terms: Public domain W3C validator