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

Theorem exbidv 1703
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 1416 . 2 (φxφ)
2 albidv.1 . 2 (φ → (ψχ))
31, 2exbidh 1502 1 (φ → (xψxχ))
Colors of variables: wff set class
Syntax hints:  wi 4  wb 98  wex 1378
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 1333  ax-gen 1335  ax-ie1 1379  ax-ie2 1380  ax-4 1397  ax-17 1416  ax-ial 1424
This theorem depends on definitions:  df-bi 110
This theorem is referenced by:  ax11ev  1706  2exbidv  1745  3exbidv  1746  eubidh  1903  eubid  1904  eleq1  2097  eleq2  2098  rexbidv2  2323  ceqsex2  2588  alexeq  2664  ceqex  2665  sbc5  2781  sbcex2  2806  sbcexg  2807  sbcabel  2833  eluni  3574  csbunig  3579  intab  3635  cbvopab1  3821  cbvopab1s  3823  axsep2  3867  zfauscl  3868  bnd2  3917  mss  3953  opeqex  3977  euotd  3982  snnex  4147  uniuni  4149  regexmid  4219  nnregexmid  4285  opeliunxp  4338  csbxpg  4364  brcog  4445  elrn2g  4468  dfdmf  4471  csbdmg  4472  eldmg  4473  dfrnf  4518  elrn2  4519  elrnmpt1  4528  brcodir  4655  xp11m  4702  xpimasn  4712  csbrng  4725  elxp4  4751  elxp5  4752  dfco2a  4764  cores  4767  funimaexglem  4925  brprcneu  5114  ssimaexg  5178  dmfco  5184  fndmdif  5215  fmptco  5273  fliftf  5382  acexmidlem2  5452  acexmidlemv  5453  cbvoprab1  5518  cbvoprab2  5519  dmtpos  5812  tfrlemi1  5887  ecdmn0m  6084  ereldm  6085  elqsn0m  6110  bren  6164  brdomg  6165  domeng  6169  recexnq  6374  prarloc  6485  genpdflem  6489  genpassl  6506  genpassu  6507  ltexprlemell  6571  ltexprlemelu  6572  ltexprlemm  6573  recexprlemell  6593  recexprlemelu  6594  bdsep2  9320  bdzfauscl  9324  strcoll2  9413
  Copyright terms: Public domain W3C validator