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

Theorem exancom 1576
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 437 . 2  |-  ( (
ph  /\  ps )  <->  ( ps  /\  ph )
)
21exbii 1572 1  |-  ( E. x ( ph  /\  ps )  <->  E. x ( ps 
/\  ph ) )
Colors of variables: wff set class
Syntax hints:    <-> wb 176    /\ wa 358   E.wex 1531
This theorem is referenced by:  19.29r  1587  19.42  1828  risset  2603  morex  2962  pwpw0  3779  pwsnALT  3838  dfuni2  3845  eluni2  3847  unipr  3857  dfiun2g  3951  uniuni  4543  cnvco  4881  imadif  5343  pceu  12915  gsumval3eu  15206  isch3  21837  brimg  24547  funpartlem  24552  isconcl7a  26208  bnj1109  29134  bnj1304  29168  bnj849  29273
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1536  ax-5 1547
This theorem depends on definitions:  df-bi 177  df-an 360  df-ex 1532
  Copyright terms: Public domain W3C validator