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

Theorem 19.42vv 1935
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 1934 . 2  |-  ( E. x E. y (
ph  /\  ps )  <->  E. x ( ph  /\  E. y ps ) )
2 19.42v 1933 . 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 1587
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1592  ax-4 1603  ax-5 1671  ax-6 1710  ax-7 1730  ax-10 1777  ax-12 1794
This theorem depends on definitions:  df-bi 185  df-an 371  df-ex 1588  df-nf 1591
This theorem is referenced by:  19.42vvv  1936  exdistr2  1937  3exdistr  1938  ceqsex3v  3110  ceqsex4v  3111  ceqsex8v  3113  elvvv  4998  xpdifid  5366  dfoprab2  6234  resoprab  6288  elrnmpt2res  6306  ov3  6329  ov6g  6330  oprabex3  6668  xpassen  7507  axaddf  9415  axmulf  9416  usgraedg4  23442  qqhval2  26547  el2wlkonot  30528  el2spthonot  30529  el2wlkonotot0  30531  bnj996  32250  dvhopellsm  35070
  Copyright terms: Public domain W3C validator