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

Theorem exancom 1596
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 1592 1  |-  ( E. x ( ph  /\  ps )  <->  E. x ( ps 
/\  ph ) )
Colors of variables: wff set class
Syntax hints:    <-> wb 177    /\ wa 359   E.wex 1550
This theorem is referenced by:  19.29r  1607  19.42  1902  risset  2745  morex  3110  pwpw0  3938  pwsnALT  4002  dfuni2  4009  eluni2  4011  unipr  4021  dfiun2g  4115  uniuni  4708  cnvco  5048  imadif  5520  pceu  13212  gsumval3eu  15505  isch3  22736  funpartlem  25779  bnj1109  29094  bnj1304  29128  bnj849  29233
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1555  ax-5 1566
This theorem depends on definitions:  df-bi 178  df-an 361  df-ex 1551
  Copyright terms: Public domain W3C validator