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

Theorem 19.42vv 1782
Description: Version of 19.42 1977 with two quantifiers and a dv condition requiring fewer axioms. (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 1781 . 2  |-  ( E. x E. y (
ph  /\  ps )  <->  E. x ( ph  /\  E. y ps ) )
2 19.42v 1780 . 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 367   E.wex 1617
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1623  ax-4 1636  ax-5 1709  ax-6 1752
This theorem depends on definitions:  df-bi 185  df-an 369  df-ex 1618
This theorem is referenced by:  19.42vvv  1783  exdistr2  1784  3exdistr  1785  ceqsex3v  3146  ceqsex4v  3147  ceqsex8v  3149  elvvv  5048  xpdifid  5420  dfoprab2  6316  resoprab  6371  elrnmpt2res  6389  ov3  6412  ov6g  6413  oprabex3  6762  xpassen  7604  axaddf  9511  axmulf  9512  usgraedg4  24589  el2wlkonot  25071  el2spthonot  25072  el2wlkonotot0  25074  qqhval2  28197  bnj996  34414  dvhopellsm  37241
  Copyright terms: Public domain W3C validator