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

Theorem exancom 1658
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 1654 1  |-  ( E. x ( ph  /\  ps )  <->  E. x ( ps 
/\  ph ) )
Colors of variables: wff setvar class
Syntax hints:    <-> wb 184    /\ wa 369   E.wex 1599
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1605  ax-4 1618
This theorem depends on definitions:  df-bi 185  df-an 371  df-ex 1600
This theorem is referenced by:  19.29r  1671  19.42v  1761  19.42  1958  eupickb  2346  risset  2968  morex  3269  pwpw0  4163  pwsnALT  4229  dfuni2  4236  eluni2  4238  unipr  4247  dfiun2g  4347  cnvco  5178  imadif  5653  uniuni  6594  pceu  14352  gsumval3eu  16886  isch3  26137  funpartlem  29568  ssfiunibd  31463  bnj1109  33713  bnj1304  33746  bnj849  33851  bj-elsngl  34409  bj-ccinftydisj  34491
  Copyright terms: Public domain W3C validator