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

Theorem 19.42vv 1850
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 1849 . 2  |-  ( E. x E. y (
ph  /\  ps )  <->  E. x ( ph  /\  E. y ps ) )
2 19.42v 1848 . 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 1528
This theorem is referenced by:  19.42vvv  1851  exdistr2  1852  3exdistr  1853  ceqsex3v  2827  ceqsex4v  2828  ceqsex8v  2830  elvvv  4748  dfoprab2  5857  resoprab  5902  oprabex3  5924  ov3  5946  ov6g  5947  xpassen  6952  axaddf  8763  axmulf  8764  brimg  23886  bnj996  28266  dvhopellsm  30586
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1533  ax-5 1544  ax-17 1603  ax-9 1636  ax-8 1644  ax-6 1704  ax-11 1716
This theorem depends on definitions:  df-bi 177  df-an 360  df-ex 1529  df-nf 1532
  Copyright terms: Public domain W3C validator