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

Theorem 19.41vv 1925
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 1924 . . 3  |-  ( E. y ( ph  /\  ps )  <->  ( E. y ph  /\  ps ) )
21exbii 1592 . 2  |-  ( E. x E. y (
ph  /\  ps )  <->  E. x ( E. y ph  /\  ps ) )
3 19.41v 1924 . 2  |-  ( E. x ( E. y ph  /\  ps )  <->  ( E. x E. y ph  /\  ps ) )
42, 3bitri 241 1  |-  ( E. x E. y (
ph  /\  ps )  <->  ( E. x E. y ph  /\  ps ) )
Colors of variables: wff set class
Syntax hints:    <-> wb 177    /\ wa 359   E.wex 1550
This theorem is referenced by:  19.41vvv  1926  pm11.07OLD  2192  rabxp  4914  mpt2mptx  6164  copsex2gb  6407  xpassen  7202  dfac5lem1  8004  3v3e3cycl  21652  dfdm5  25400  dfrn5  25401  elima4  25404  brtxp2  25726  brpprod3a  25731  brimg  25782  brsuccf  25786  bnj996  29326  diblsmopel  31969
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1555  ax-5 1566  ax-17 1626  ax-9 1666  ax-8 1687  ax-6 1744  ax-11 1761
This theorem depends on definitions:  df-bi 178  df-an 361  df-ex 1551  df-nf 1554
  Copyright terms: Public domain W3C validator