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

Theorem 19.41vv 2035
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 2034 . . 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 2034 . 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  2036  pm11.07  2075  rabxp  4632  mpt2mptx  5790  copsex2gb  6032  xpassen  6841  dfac5lem1  7634  dfdm5  23300  dfrn5  23301  brtxp2  23596  brpprod3a  23601  brimg  23650  brsuccf  23654  dfoprab4pop  24202  bnj996  27773  diblsmopel  30265
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