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

Theorem 19.42vv 1825
Description: Version of 19.42 2026 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 1824 . 2  |-  ( E. x E. y (
ph  /\  ps )  <->  E. x ( ph  /\  E. y ps ) )
2 19.42v 1823 . 2  |-  ( E. x ( ph  /\  E. y ps )  <->  ( ph  /\ 
E. x E. y ps ) )
31, 2bitri 252 1  |-  ( E. x E. y (
ph  /\  ps )  <->  (
ph  /\  E. x E. y ps ) )
Colors of variables: wff setvar class
Syntax hints:    <-> wb 187    /\ wa 370   E.wex 1659
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1665  ax-4 1678  ax-5 1748  ax-6 1794
This theorem depends on definitions:  df-bi 188  df-an 372  df-ex 1660
This theorem is referenced by:  19.42vvv  1826  exdistr2  1827  3exdistr  1828  ceqsex3v  3118  ceqsex4v  3119  ceqsex8v  3121  elvvv  4905  xpdifid  5276  dfoprab2  6342  resoprab  6397  elrnmpt2res  6415  ov3  6438  ov6g  6439  oprabex3  6787  xpassen  7663  axaddf  9558  axmulf  9559  usgraedg4  24957  el2wlkonot  25439  el2spthonot  25440  el2wlkonotot0  25442  qqhval2  28622  bnj996  29551  dvhopellsm  34394
  Copyright terms: Public domain W3C validator