ILE Home Intuitionistic Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  ILE Home  >  Th. List  >  exbidv Structured version   GIF version

Theorem exbidv 1688
Description: Formula-building rule for existential quantifier (deduction rule). (Contributed by NM, 5-Aug-1993.)
Hypothesis
Ref Expression
albidv.1 (φ → (ψχ))
Assertion
Ref Expression
exbidv (φ → (xψxχ))
Distinct variable group:   φ,x
Allowed substitution hints:   ψ(x)   χ(x)

Proof of Theorem exbidv
StepHypRef Expression
1 ax-17 1400 . 2 (φxφ)
2 albidv.1 . 2 (φ → (ψχ))
31, 2exbidh 1487 1 (φ → (xψxχ))
Colors of variables: wff set class
Syntax hints:  wi 4  wb 98  wex 1362
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 99  ax-ia2 100  ax-ia3 101  ax-5 1316  ax-gen 1318  ax-ie1 1363  ax-ie2 1364  ax-4 1381  ax-17 1400  ax-ial 1409
This theorem depends on definitions:  df-bi 110
This theorem is referenced by:  ax11ev  1691  2exbidv  1730  3exbidv  1731  eubidh  1888  eubid  1889  eleq1  2082  eleq2  2083  rexbidv2  2307  ceqsex2  2571  alexeq  2647  ceqex  2648  sbc5  2764  sbcex2  2789  sbcexg  2790  sbcabel  2816  eluni  3557  csbunig  3562  intab  3618  cbvopab1  3804  cbvopab1s  3806  axsep2  3850  zfauscl  3851  bnd2  3900  mss  3936  opeqex  3960  euotd  3965  snnex  4131  uniuni  4133  regexmid  4203  nnregexmid  4269  opeliunxp  4322  csbxpg  4348  brcog  4429  elrn2g  4452  dfdmf  4455  csbdmg  4456  eldmg  4457  dfrnf  4502  elrn2  4503  elrnmpt1  4512  brcodir  4639  xp11m  4686  xpimasn  4696  csbrng  4709  elxp4  4735  elxp5  4736  dfco2a  4748  cores  4751  funimaexglem  4908  brprcneu  5096  ssimaexg  5160  dmfco  5166  fndmdif  5197  fmptco  5255  fliftf  5364  acexmidlem2  5433  acexmidlemv  5434  cbvoprab1  5499  cbvoprab2  5500  dmtpos  5793  tfrlemi1  5867  tfrlemi14  5869  ecdmn0m  6059  ereldm  6060  elqsn0m  6085  recex  6249  prarloc  6357  genpdflem  6361  genpassl  6379  genpassu  6380  ltexprlemell  6435  ltexprlemelu  6436  ltexprlemm  6437  recexprlemell  6456  recexprlemelu  6457  bdsep2  7112  bdzfauscl  7116  strcoll2  7201
  Copyright terms: Public domain W3C validator