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

Theorem exancom 1679
Description: Commutation of conjunction inside an existential quantifier. (Contributed by NM, 18-Aug-1993.)
Assertion
Ref Expression
exancom  |-  ( E. x ( ph  /\  ps )  <->  E. x ( ps 
/\  ph ) )

Proof of Theorem exancom
StepHypRef Expression
1 ancom 448 . 2  |-  ( (
ph  /\  ps )  <->  ( ps  /\  ph )
)
21exbii 1675 1  |-  ( E. x ( ph  /\  ps )  <->  E. x ( ps 
/\  ph ) )
Colors of variables: wff setvar class
Syntax hints:    <-> wb 184    /\ wa 367   E.wex 1620
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1626  ax-4 1639
This theorem depends on definitions:  df-bi 185  df-an 369  df-ex 1621
This theorem is referenced by:  19.29r  1692  19.42v  1783  19.42  1980  eupickb  2291  risset  2907  morex  3208  pwpw0  4092  pwsnALT  4158  dfuni2  4165  eluni2  4167  unipr  4176  dfiun2g  4275  cnvco  5101  imadif  5571  uniuni  6508  pceu  14372  gsumval3eu  17024  isch3  26276  funpartlem  29745  ssfiunibd  31675  bnj1109  34192  bnj1304  34225  bnj849  34330  bj-elsngl  34874  bj-ccinftydisj  34963
  Copyright terms: Public domain W3C validator