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

Theorem 19.41vv 1855
Description: Theorem 19.41 of [Margaris] p. 90 with 2 quantifiers. (Contributed by NM, 30-Apr-1995.)
Assertion
Ref Expression
19.41vv  |-  ( E. x E. y (
ph  /\  ps )  <->  ( E. x E. y ph  /\  ps ) )
Distinct variable groups:    ps, x    ps, y
Allowed substitution hints:    ph( x, y)

Proof of Theorem 19.41vv
StepHypRef Expression
1 19.41v 1854 . . 3  |-  ( E. y ( ph  /\  ps )  <->  ( E. y ph  /\  ps ) )
21exbii 1572 . 2  |-  ( E. x E. y (
ph  /\  ps )  <->  E. x ( E. y ph  /\  ps ) )
3 19.41v 1854 . 2  |-  ( E. x ( E. y ph  /\  ps )  <->  ( E. x E. y ph  /\  ps ) )
42, 3bitri 240 1  |-  ( E. x E. y (
ph  /\  ps )  <->  ( E. x E. y ph  /\  ps ) )
Colors of variables: wff set class
Syntax hints:    <-> wb 176    /\ wa 358   E.wex 1531
This theorem is referenced by:  19.41vvv  1856  pm11.07  2067  rabxp  4741  mpt2mptx  5954  copsex2gb  6196  xpassen  6972  dfac5lem1  7766  dfdm5  24203  dfrn5  24204  brtxp2  24492  brpprod3a  24497  brimg  24547  brsuccf  24551  dfoprab4pop  25140  bnj996  29303  pm11.07OLD7  29716  diblsmopel  31983
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1536  ax-5 1547  ax-17 1606  ax-9 1644  ax-8 1661  ax-6 1715  ax-11 1727
This theorem depends on definitions:  df-bi 177  df-an 360  df-ex 1532  df-nf 1535
  Copyright terms: Public domain W3C validator