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

Theorem 19.41vv 2036
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 2035 . . 3  |-  ( E. y ( ph  /\  ps )  <->  ( E. y ph  /\  ps ) )
21exbii 1580 . 2  |-  ( E. x E. y (
ph  /\  ps )  <->  E. x ( E. y ph  /\  ps ) )
3 19.41v 2035 . 2  |-  ( E. x ( E. y ph  /\  ps )  <->  ( E. x E. y ph  /\  ps ) )
42, 3bitri 242 1  |-  ( E. x E. y (
ph  /\  ps )  <->  ( E. x E. y ph  /\  ps ) )
Colors of variables: wff set class
Syntax hints:    <-> wb 178    /\ wa 360   E.wex 1537
This theorem is referenced by:  19.41vvv  2037  pm11.07  2078  rabxp  4699  mpt2mptx  5858  copsex2gb  6100  xpassen  6910  dfac5lem1  7704  dfdm5  23487  dfrn5  23488  brtxp2  23783  brpprod3a  23788  brimg  23837  brsuccf  23841  dfoprab4pop  24389  bnj996  28020  diblsmopel  30512
This theorem was proved from axioms:  ax-1 7  ax-2 8  ax-3 9  ax-mp 10  ax-5 1533  ax-6 1534  ax-gen 1536  ax-17 1628  ax-4 1692
This theorem depends on definitions:  df-bi 179  df-an 362  df-ex 1538  df-nf 1540
  Copyright terms: Public domain W3C validator