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

Theorem exancom 1638
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 1634 1  |-  ( E. x ( ph  /\  ps )  <->  E. x ( ps 
/\  ph ) )
Colors of variables: wff setvar class
Syntax hints:    <-> wb 184    /\ wa 369   E.wex 1586
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1591  ax-4 1602
This theorem depends on definitions:  df-bi 185  df-an 371  df-ex 1587
This theorem is referenced by:  19.29r  1651  19.42  1900  eupickb  2344  risset  2761  morex  3141  pwpw0  4019  pwsnALT  4084  dfuni2  4091  eluni2  4093  unipr  4102  dfiun2g  4200  cnvco  5023  imadif  5491  uniuni  6383  pceu  13911  gsumval3eu  16379  isch3  24642  funpartlem  27971  bnj1109  31777  bnj1304  31810  bnj849  31915  bj-elsngl  32458  bj-ccinftydisj  32533
  Copyright terms: Public domain W3C validator