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

Theorem 19.42vv 1917
Description: Theorem 19.42 of [Margaris] p. 90 with 2 quantifiers. (Contributed by NM, 16-Mar-1995.)
Assertion
Ref Expression
19.42vv  |-  ( E. x E. y (
ph  /\  ps )  <->  (
ph  /\  E. x E. y ps ) )
Distinct variable groups:    ph, x    ph, y
Allowed substitution hints:    ps( x, y)

Proof of Theorem 19.42vv
StepHypRef Expression
1 exdistr 1916 . 2  |-  ( E. x E. y (
ph  /\  ps )  <->  E. x ( ph  /\  E. y ps ) )
2 19.42v 1915 . 2  |-  ( E. x ( ph  /\  E. y ps )  <->  ( ph  /\ 
E. x E. y ps ) )
31, 2bitri 240 1  |-  ( E. x E. y (
ph  /\  ps )  <->  (
ph  /\  E. x E. y ps ) )
Colors of variables: wff set class
Syntax hints:    <-> wb 176    /\ wa 358   E.wex 1546
This theorem is referenced by:  19.42vvv  1918  exdistr2  1919  3exdistr  1920  ceqsex3v  2911  ceqsex4v  2912  ceqsex8v  2914  elvvv  4852  dfoprab2  6021  resoprab  6066  oprabex3  6088  ov3  6110  ov6g  6111  xpassen  7099  axaddf  8914  axmulf  8915  usgraedg4  21083  qqhval2  23959  brimg  25302  bnj996  28739  dvhopellsm  31366
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1551  ax-5 1562  ax-17 1621  ax-9 1659  ax-8 1680  ax-6 1734  ax-11 1751
This theorem depends on definitions:  df-bi 177  df-an 360  df-ex 1547  df-nf 1550
  Copyright terms: Public domain W3C validator