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

Theorem 2exbidv 1618
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 1616 . 2  |-  ( ph  ->  ( E. y ps  <->  E. y ch ) )
32exbidv 1616 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 1531
This theorem is referenced by:  3exbidv  1619  4exbidv  1620  cbvex4v  1965  ceqsex3v  2839  ceqsex4v  2840  2reu5  2986  copsexg  4268  euotd  4283  elopab  4288  elxpi  4721  relop  4850  cbvoprab3  5938  ov6g  6001  th3qlem1  6780  omxpenlem  6979  dcomex  8089  ltresr  8778  fsumcom2  12253  ispos  14097  fsumvma  20468  dfres3  24187  itg2addnc  25005  2sbc5g  27719  cbvex4vOLD7  29692  dvhopellsm  31929  diblsmopel  31983
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1536  ax-5 1547  ax-17 1606
This theorem depends on definitions:  df-bi 177  df-ex 1532
  Copyright terms: Public domain W3C validator