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

Theorem exancom 1861
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 460 . 2 ((𝜑𝜓) ↔ (𝜓𝜑))
21exbii 1848 1 (∃𝑥(𝜑𝜓) ↔ ∃𝑥(𝜓𝜑))
Colors of variables: wff setvar class
Syntax hints:  wb 206  wa 395  wex 1779
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809
This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1780
This theorem is referenced by:  19.42v  1953  19.42  2237  eupickb  2628  datisi  2673  disamis  2674  dimatis  2681  fresison  2682  bamalip  2685  risset  3204  morex  3679  pwpw0  4764  dfuni2  4860  eluni2  4862  cnvco  5828  imadif  6566  uniuni  7698  pceu  16758  gsumval3eu  19783  isch3  31185  tgoldbachgt  34631  bnj1109  34753  bnj1304  34786  bnj849  34892  onvf1odlem1  35080  funpartlem  35920  bj-19.41t  36752  bj-elsngl  36946  bj-ccinftydisj  37191  mopickr  38335  moantr  38336  brcosscnvcoss  38415  rr-groth  44276  rr-grothshortbi  44280  eluni2f  45085  ssfiunibd  45295  setrec1lem3  49678
  Copyright terms: Public domain W3C validator