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

Theorem 2exbidv 1614
Description: Formula-building rule for 2 existential quantifiers (deduction rule). (Contributed by NM, 1-May-1995.)
Hypothesis
Ref Expression
2albidv.1  |-  ( ph  ->  ( ps  <->  ch )
)
Assertion
Ref Expression
2exbidv  |-  ( ph  ->  ( E. x E. y ps  <->  E. x E. y ch ) )
Distinct variable groups:    ph, x    ph, y
Allowed substitution hints:    ps( x, y)    ch( x, y)

Proof of Theorem 2exbidv
StepHypRef Expression
1 2albidv.1 . . 3  |-  ( ph  ->  ( ps  <->  ch )
)
21exbidv 1612 . 2  |-  ( ph  ->  ( E. y ps  <->  E. y ch ) )
32exbidv 1612 1  |-  ( ph  ->  ( E. x E. y ps  <->  E. x E. y ch ) )
Colors of variables: wff set class
Syntax hints:    -> wi 4    <-> wb 176   E.wex 1528
This theorem is referenced by:  3exbidv  1615  4exbidv  1616  cbvex4v  1952  ceqsex3v  2826  ceqsex4v  2827  2reu5  2973  copsexg  4252  euotd  4267  elopab  4272  elxpi  4705  relop  4834  cbvoprab3  5922  ov6g  5985  th3qlem1  6764  omxpenlem  6963  dcomex  8073  ltresr  8762  fsumcom2  12237  ispos  14081  fsumvma  20452  dfres3  24116  2sbc5g  27616  dvhopellsm  31307  diblsmopel  31361
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1533  ax-5 1544  ax-17 1603
This theorem depends on definitions:  df-bi 177  df-ex 1529
  Copyright terms: Public domain W3C validator