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

Theorem 2exbidv 1928
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 1925 . 2 (𝜑 → (∃𝑦𝜓 ↔ ∃𝑦𝜒))
32exbidv 1925 1 (𝜑 → (∃𝑥𝑦𝜓 ↔ ∃𝑥𝑦𝜒))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 205  wex 1782
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914
This theorem depends on definitions:  df-bi 206  df-ex 1783
This theorem is referenced by:  3exbidv  1929  4exbidv  1930  cbvex4vw  2046  cbvex4v  2415  ceqsex3v  3530  ceqsex4v  3531  2reu5  3752  opabbidv  5210  unopab  5226  copsexgw  5486  copsexg  5487  euotd  5509  elopabw  5522  elxpi  5694  relop  5845  dfres3  5981  xpdifid  6159  oprabv  7456  cbvoprab3  7487  elrnmpores  7533  ov6g  7558  omxpenlem  9061  dcomex  10429  ltresr  11122  hashle2prv  14426  fsumcom2  15707  fprodcom2  15915  ispos  18254  fsumvma  26683  1pthon2v  29373  dfconngr1  29408  isconngr  29409  isconngr1  29410  1conngr  29414  conngrv2edg  29415  fusgr2wsp2nb  29554  isacycgr  34067  satfv1  34285  sat1el2xp  34301  elfuns  34818  bj-cbvex4vv  35588  itg2addnclem3  36446  brxrn2  37151  dvhopellsm  39894  diblsmopel  39948  2sbc5g  43046  fundcmpsurinj  45950  ichexmpl1  46010  ichnreuop  46013  ichreuopeq  46014  elsprel  46016  prprelb  46057  reuopreuprim  46067
  Copyright terms: Public domain W3C validator