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

Theorem 2exbidv 1854
Description: Formula-building rule for two existential quantifiers (deduction rule). (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 1852 . 2 (𝜑 → (∃𝑦𝜓 ↔ ∃𝑦𝜒))
32exbidv 1852 1 (𝜑 → (∃𝑥𝑦𝜓 ↔ ∃𝑥𝑦𝜒))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 196  wex 1701
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1719  ax-4 1734  ax-5 1841
This theorem depends on definitions:  df-bi 197  df-ex 1702
This theorem is referenced by:  3exbidv  1855  4exbidv  1856  cbvex4v  2293  ceqsex3v  3237  ceqsex4v  3238  2reu5  3403  copsexg  4921  euotd  4940  elopab  4948  elxpi  5095  relop  5237  xpdifid  5525  oprabv  6657  cbvoprab3  6685  elrnmpt2res  6728  ov6g  6752  omxpenlem  8006  dcomex  9214  ltresr  9906  fsumcom2  14428  fsumcom2OLD  14429  fprodcom2  14634  fprodcom2OLD  14635  ispos  16863  fsumvma  24833  1pthon2v  26873  dfconngr1  26908  isconngr  26909  isconngr1  26910  1conngr  26914  conngrv2edg  26915  fusgr2wsp2nb  27050  dfres3  31349  elfuns  31656  bj-cbvex4vv  32377  itg2addnclem3  33081  dvhopellsm  35872  diblsmopel  35926  2sbc5g  38085  elsprel  41001
  Copyright terms: Public domain W3C validator