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

Theorem 19.41vv 1845
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 1844 . . 3  |-  ( E. y ( ph  /\  ps )  <->  ( E. y ph  /\  ps ) )
21exbii 1570 . 2  |-  ( E. x E. y (
ph  /\  ps )  <->  E. x ( E. y ph  /\  ps ) )
3 19.41v 1844 . 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 1529
This theorem is referenced by:  19.41vvv  1846  pm11.07  2058  rabxp  4725  mpt2mptx  5900  copsex2gb  6142  xpassen  6952  dfac5lem1  7746  dfdm5  23534  dfrn5  23535  brtxp2  23830  brpprod3a  23835  brimg  23884  brsuccf  23888  dfoprab4pop  24436  bnj996  28255  diblsmopel  30629
This theorem was proved from axioms:  ax-1 7  ax-2 8  ax-3 9  ax-mp 10  ax-gen 1534  ax-5 1545  ax-17 1604  ax-9 1637  ax-8 1645  ax-6 1704  ax-11 1716
This theorem depends on definitions:  df-bi 179  df-an 362  df-ex 1530  df-nf 1533
  Copyright terms: Public domain W3C validator