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

Theorem 19.41vv 1756
Description: Version of 19.41 1955 with two quantifiers and a dv condition requiring fewer axioms. (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 1755 . . 3  |-  ( E. y ( ph  /\  ps )  <->  ( E. y ph  /\  ps ) )
21exbii 1652 . 2  |-  ( E. x E. y (
ph  /\  ps )  <->  E. x ( E. y ph  /\  ps ) )
3 19.41v 1755 . 2  |-  ( E. x ( E. y ph  /\  ps )  <->  ( E. x E. y ph  /\  ps ) )
42, 3bitri 249 1  |-  ( E. x E. y (
ph  /\  ps )  <->  ( E. x E. y ph  /\  ps ) )
Colors of variables: wff setvar class
Syntax hints:    <-> wb 184    /\ wa 369   E.wex 1597
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1603  ax-4 1616  ax-5 1689  ax-6 1732
This theorem depends on definitions:  df-bi 185  df-an 371  df-ex 1598
This theorem is referenced by:  19.41vvv  1757  rabxp  5023  copsex2gb  5100  mpt2mptx  6375  xpassen  7610  dfac5lem1  8504  3v3e3cycl  24534  dfdm5  29178  dfrn5  29179  elima4  29181  brtxp2  29503  brpprod3a  29508  brimg  29559  brsuccf  29563  mpt2mptx2  32652  bnj996  33741  diblsmopel  36621
  Copyright terms: Public domain W3C validator