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

Theorem exancom 1643
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 450 . 2  |-  ( (
ph  /\  ps )  <->  ( ps  /\  ph )
)
21exbii 1639 1  |-  ( E. x ( ph  /\  ps )  <->  E. x ( ps 
/\  ph ) )
Colors of variables: wff setvar class
Syntax hints:    <-> wb 184    /\ wa 369   E.wex 1591
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1596  ax-4 1607
This theorem depends on definitions:  df-bi 185  df-an 371  df-ex 1592
This theorem is referenced by:  19.29r  1656  19.42  1916  eupickb  2359  risset  2980  morex  3280  pwpw0  4168  pwsnALT  4233  dfuni2  4240  eluni2  4242  unipr  4251  dfiun2g  4350  cnvco  5179  imadif  5654  uniuni  6580  pceu  14218  gsumval3eu  16691  isch3  25821  funpartlem  29155  bnj1109  32799  bnj1304  32832  bnj849  32937  bj-elsngl  33482  bj-ccinftydisj  33563
  Copyright terms: Public domain W3C validator