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

Theorem exancom 1671
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 450 . 2
21exbii 1667 1
Colors of variables: wff setvar class
Syntax hints:  <->wb 184  /\wa 369  E.wex 1612
This theorem is referenced by:  19.29r  1684  19.42v  1775  19.42  1972  eupickb  2360  risset  2982  morex  3283  pwpw0  4178  pwsnALT  4244  dfuni2  4251  eluni2  4253  unipr  4262  dfiun2g  4362  cnvco  5193  imadif  5668  uniuni  6609  pceu  14370  gsumval3eu  16907  isch3  26159  funpartlem  29592  ssfiunibd  31509  bnj1109  33845  bnj1304  33878  bnj849  33983  bj-elsngl  34526  bj-ccinftydisj  34616
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1618  ax-4 1631
This theorem depends on definitions:  df-bi 185  df-an 371  df-ex 1613
  Copyright terms: Public domain W3C validator