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

Theorem 2exbidv 1924
Description: Formula-building rule for two existential quantifiers (deduction form). (Contributed by NM, 1-May-1995.)
Hypothesis
Ref Expression
2albidv.1 (𝜑 → (𝜓𝜒))
Assertion
Ref Expression
2exbidv (𝜑 → (∃𝑥𝑦𝜓 ↔ ∃𝑥𝑦𝜒))
Distinct variable groups:   𝜑,𝑥   𝜑,𝑦
Allowed substitution hints:   𝜓(𝑥,𝑦)   𝜒(𝑥,𝑦)

Proof of Theorem 2exbidv
StepHypRef Expression
1 2albidv.1 . . 3 (𝜑 → (𝜓𝜒))
21exbidv 1921 . 2 (𝜑 → (∃𝑦𝜓 ↔ ∃𝑦𝜒))
32exbidv 1921 1 (𝜑 → (∃𝑥𝑦𝜓 ↔ ∃𝑥𝑦𝜒))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 206  wex 1779
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910
This theorem depends on definitions:  df-bi 207  df-ex 1780
This theorem is referenced by:  3exbidv  1925  4exbidv  1926  cbvex4vw  2041  cbvex4v  2420  ceqsex3v  3537  ceqsex4v  3538  2reu5  3764  opabbidv  5209  unopab  5224  copsexgw  5495  copsexg  5496  euotd  5518  elopabw  5531  elxpi  5707  relop  5861  dfres3  6002  xpdifid  6188  oprabv  7493  cbvoprab3  7524  elrnmpores  7571  ov6g  7597  omxpenlem  9113  dcomex  10487  ltresr  11180  hashle2prv  14517  fsumcom2  15810  fprodcom2  16020  ispos  18360  fsumvma  27257  1pthon2v  30172  dfconngr1  30207  isconngr  30208  isconngr1  30209  1conngr  30213  conngrv2edg  30214  fusgr2wsp2nb  30353  isacycgr  35150  satfv1  35368  sat1el2xp  35384  elfuns  35916  cbvoprab1vw  36238  cbvoprab1davw  36272  cbvoprab3davw  36274  bj-cbvex4vv  36806  itg2addnclem3  37680  brxrn2  38376  dvhopellsm  41119  diblsmopel  41173  2sbc5g  44435  fundcmpsurinj  47396  ichexmpl1  47456  ichnreuop  47459  ichreuopeq  47460  elsprel  47462  prprelb  47503  reuopreuprim  47513
  Copyright terms: Public domain W3C validator