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

Theorem exancom 1730
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 457 . 2  |-  ( (
ph  /\  ps )  <->  ( ps  /\  ph )
)
21exbii 1726 1  |-  ( E. x ( ph  /\  ps )  <->  E. x ( ps 
/\  ph ) )
Colors of variables: wff setvar class
Syntax hints:    <-> wb 189    /\ wa 376   E.wex 1671
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1677  ax-4 1690
This theorem depends on definitions:  df-bi 190  df-an 378  df-ex 1672
This theorem is referenced by:  19.29rOLD  1745  19.42v  1842  19.42  2071  eupickb  2387  risset  2902  morex  3210  pwpw0  4111  pwsnALT  4185  dfuni2  4192  eluni2  4194  unipr  4203  dfiun2g  4301  cnvco  5025  imadif  5668  uniuni  6619  pceu  14875  gsumval3eu  17616  isch3  26975  bnj1109  29670  bnj1304  29703  bnj849  29808  funpartlem  30780  bj-elsngl  31632  bj-ccinftydisj  31725  ssfiunibd  37615
  Copyright terms: Public domain W3C validator