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

Theorem 19.42vv 1944
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 1943 . 2  |-  ( E. x E. y (
ph  /\  ps )  <->  E. x ( ph  /\  E. y ps ) )
2 19.42v 1942 . 2  |-  ( E. x ( ph  /\  E. y ps )  <->  ( ph  /\ 
E. x E. y ps ) )
31, 2bitri 249 1  |-  ( E. x E. y (
ph  /\  ps )  <->  (
ph  /\  E. x E. y ps ) )
Colors of variables: wff setvar class
Syntax hints:    <-> wb 184    /\ wa 369   E.wex 1591
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1596  ax-4 1607  ax-5 1675  ax-6 1714  ax-7 1734  ax-10 1781  ax-12 1798
This theorem depends on definitions:  df-bi 185  df-an 371  df-ex 1592  df-nf 1595
This theorem is referenced by:  19.42vvv  1945  exdistr2  1946  3exdistr  1947  ceqsex3v  3146  ceqsex4v  3147  ceqsex8v  3149  elvvv  5051  xpdifid  5426  dfoprab2  6318  resoprab  6373  elrnmpt2res  6391  ov3  6414  ov6g  6415  oprabex3  6763  xpassen  7601  axaddf  9511  axmulf  9512  usgraedg4  24049  el2wlkonot  24531  el2spthonot  24532  el2wlkonotot0  24534  qqhval2  27585  bnj996  32967  dvhopellsm  35789
  Copyright terms: Public domain W3C validator