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

Theorem 2exbidv 1687
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 1685 . 2  |-  ( ph  ->  ( E. y ps  <->  E. y ch ) )
32exbidv 1685 1  |-  ( ph  ->  ( E. x E. y ps  <->  E. x E. y ch ) )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    <-> wb 184   E.wex 1591
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1596  ax-4 1607  ax-5 1675
This theorem depends on definitions:  df-bi 185  df-ex 1592
This theorem is referenced by:  3exbidv  1688  4exbidv  1689  cbvex4v  1987  ceqsex3v  3009  ceqsex4v  3010  2reu5  3164  copsexg  4573  copsexgOLD  4574  euotd  4589  elopab  4594  elxpi  4852  relop  4986  xpdifid  5263  cbvoprab3  6161  elrnmpt2res  6203  ov6g  6227  th3qlem1  7202  omxpenlem  7408  dcomex  8612  ltresr  9303  fsumcom2  13237  ispos  15113  fsumvma  22511  dfconngra1  23492  isconngra  23493  isconngra1  23494  1conngra  23496  fprodcom2  27424  dfres3  27498  elfuns  27875  itg2addnclem3  28370  2sbc5g  29595  oprabv  30082  is2wlkonot  30307  is2spthonot  30308  2wlkonot  30309  2spthonot  30310  el2wlkonot  30313  el2spthonot  30314  el2spthonot0  30315  el2wlkonotot0  30316  2wlkonot3v  30319  2spthonot3v  30320  usg2wotspth  30328  2pthwlkonot  30329  2spotdisj  30579  usg2spot2nb  30583  bj-cbvex4vv  32007  dvhopellsm  34484  diblsmopel  34538
  Copyright terms: Public domain W3C validator