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  2236  eupickb  2635  datisi  2680  disamis  2681  dimatis  2688  fresison  2689  bamalip  2692  risset  3233  morex  3725  pwpw0  4813  dfuni2  4909  eluni2  4911  dfiun2gOLD  5031  cnvco  5896  imadif  6650  uniuni  7782  pceu  16884  gsumval3eu  19922  isch3  31260  tgoldbachgt  34678  bnj1109  34800  bnj1304  34833  bnj849  34939  funpartlem  35943  bj-19.41t  36775  bj-elsngl  36969  bj-ccinftydisj  37214  mopickr  38364  moantr  38365  brcosscnvcoss  38435  rr-groth  44318  rr-grothshortbi  44322  eluni2f  45108  ssfiunibd  45321  setrec1lem3  49208
  Copyright terms: Public domain W3C validator