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

Theorem exancom 1593
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 438 . 2  |-  ( (
ph  /\  ps )  <->  ( ps  /\  ph )
)
21exbii 1589 1  |-  ( E. x ( ph  /\  ps )  <->  E. x ( ps 
/\  ph ) )
Colors of variables: wff set class
Syntax hints:    <-> wb 177    /\ wa 359   E.wex 1547
This theorem is referenced by:  19.29r  1604  19.42  1891  risset  2697  morex  3062  pwpw0  3890  pwsnALT  3953  dfuni2  3960  eluni2  3962  unipr  3972  dfiun2g  4066  uniuni  4657  cnvco  4997  imadif  5469  pceu  13148  gsumval3eu  15441  isch3  22593  brimg  25501  funpartlem  25506  bnj1109  28496  bnj1304  28530  bnj849  28635
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1552  ax-5 1563
This theorem depends on definitions:  df-bi 178  df-an 361  df-ex 1548
  Copyright terms: Public domain W3C validator