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

Theorem 19.42vv 1930
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 1929 . 2  |-  ( E. x E. y (
ph  /\  ps )  <->  E. x ( ph  /\  E. y ps ) )
2 19.42v 1928 . 2  |-  ( E. x ( ph  /\  E. y ps )  <->  ( ph  /\ 
E. x E. y ps ) )
31, 2bitri 241 1  |-  ( E. x E. y (
ph  /\  ps )  <->  (
ph  /\  E. x E. y ps ) )
Colors of variables: wff set class
Syntax hints:    <-> wb 177    /\ wa 359   E.wex 1550
This theorem is referenced by:  19.42vvv  1931  exdistr2  1932  3exdistr  1933  ceqsex3v  2994  ceqsex4v  2995  ceqsex8v  2997  elvvv  4937  dfoprab2  6121  resoprab  6166  oprabex3  6188  ov3  6210  ov6g  6211  xpassen  7202  axaddf  9020  axmulf  9021  usgraedg4  21406  qqhval2  24366  el2wlkonot  28336  el2spthonot  28337  el2wlkonotot0  28339  bnj996  29326  dvhopellsm  31915
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1555  ax-5 1566  ax-17 1626  ax-9 1666  ax-8 1687  ax-6 1744  ax-11 1761
This theorem depends on definitions:  df-bi 178  df-an 361  df-ex 1551  df-nf 1554
  Copyright terms: Public domain W3C validator