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

Theorem exancom 1573
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 1569 1  |-  ( E. x ( ph  /\  ps )  <->  E. x ( ps 
/\  ph ) )
Colors of variables: wff set class
Syntax hints:    <-> wb 176    /\ wa 358   E.wex 1528
This theorem is referenced by:  19.29r  1584  19.42  1816  risset  2590  morex  2949  pwpw0  3763  pwsnALT  3822  dfuni2  3829  eluni2  3831  unipr  3841  dfiun2g  3935  uniuni  4527  cnvco  4865  imadif  5327  pceu  12899  gsumval3eu  15190  isch3  21821  brimg  24476  isconcl7a  26105  bnj1109  28818  bnj1304  28852  bnj849  28957
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1533  ax-5 1544
This theorem depends on definitions:  df-bi 177  df-an 360  df-ex 1529
  Copyright terms: Public domain W3C validator