NFE Home New Foundations Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  NFE Home  >  Th. List  >  2exbidv GIF version

Theorem 2exbidv 1628
Description: Formula-building rule for 2 existential quantifiers (deduction rule). (Contributed by NM, 1-May-1995.)
Hypothesis
Ref Expression
2albidv.1 (φ → (ψχ))
Assertion
Ref Expression
2exbidv (φ → (xyψxyχ))
Distinct variable groups:   φ,x   φ,y
Allowed substitution hints:   ψ(x,y)   χ(x,y)

Proof of Theorem 2exbidv
StepHypRef Expression
1 2albidv.1 . . 3 (φ → (ψχ))
21exbidv 1626 . 2 (φ → (yψyχ))
32exbidv 1626 1 (φ → (xyψxyχ))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 176  wex 1541
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1546  ax-5 1557  ax-17 1616
This theorem depends on definitions:  df-bi 177  df-ex 1542
This theorem is referenced by:  3exbidv  1629  4exbidv  1630  cbvex4v  2012  ceqsex3v  2897  ceqsex4v  2898  2reu5  3044  elxpk  4196  cnvkeq  4215  ins2keq  4218  ins3keq  4219  sikeq  4241  opkelopkabg  4245  otkelins2kg  4253  otkelins3kg  4254  opkelcokg  4261  opkelsikg  4264  sikss1c1c  4267  copsexg  4607  elopab  4696  brsi  4761  elxpi  4800  brswap2  4860  brswap  5509  cbvoprab3  5571  ov6g  5600  brsnsi  5773  dmpprod  5840  ovce  6172  ceex  6174  elce  6175
  Copyright terms: Public domain W3C validator