Theorem exbidv 1746

Description: Formula-building rule for existential quantifier (deduction rule). (Contributed by NM, 5-Aug-1993.)

Hypothesis

Ref	Expression
albidv.1	|- ( ph -> ( ps <-> ch ) )

Assertion

Ref	Expression
exbidv	|- ( ph -> ( E. x ps <-> E. x ch ) )

Distinct variable group:   ph, x

Allowed substitution hints:   ps( x)   ch( x)

Proof of Theorem exbidv

Step	Hyp	Ref	Expression
1		ax-17 1459	. 2 |- ( ph -> A. x ph )
2		albidv.1	. 2 |- ( ph -> ( ps <-> ch ) )
3	1, 2	exbidh 1545	1 |- ( ph -> ( E. x ps <-> E. x ch ) )

Syntax hints:   -> wi 4   <-> wb 103   E.wex 1421

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 104  ax-ia2 105  ax-ia3 106  ax-5 1376  ax-gen 1378  ax-ie1 1422  ax-ie2 1423  ax-4 1440  ax-17 1459  ax-ial 1467

This theorem depends on definitions:  df-bi 115

This theorem is referenced by:  ax11ev  1749  2exbidv  1789  3exbidv  1790  eubidh  1947  eubid  1948  eleq1  2141  eleq2  2142  rexbidv2  2371  ceqsex2  2639  alexeq  2721  ceqex  2722  sbc5  2838  sbcex2  2867  sbcexg  2868  sbcabel  2895  eluni  3604  csbunig  3609  intab  3665  cbvopab1  3851  cbvopab1s  3853  axsep2  3897  zfauscl  3898  bnd2  3947  mss  3981  opeqex  4004  euotd  4009  snnex  4199  uniuni  4201  regexmid  4278  reg2exmid  4279  onintexmid  4315  reg3exmid  4322  nnregexmid  4360  opeliunxp  4413  csbxpg  4439  brcog  4520  elrn2g  4543  dfdmf  4546  csbdmg  4547  eldmg  4548  dfrnf  4593  elrn2  4594  elrnmpt1  4603  brcodir  4732  xp11m  4779  xpimasn  4789  csbrng  4802  elxp4  4828  elxp5  4829  dfco2a  4841  cores  4844  funimaexglem  5002  brprcneu  5191  ssimaexg  5256  dmfco  5262  fndmdif  5293  fmptco  5351  fliftf  5459  acexmidlem2  5529  acexmidlemv  5530  cbvoprab1  5596  cbvoprab2  5597  dmtpos  5894  tfrlemi1  5969  ecdmn0m  6171  ereldm  6172  elqsn0m  6197  bren  6251  brdomg  6252  domeng  6256  ac6sfi  6379  ordiso  6447  recexnq  6580  prarloc  6693  genpdflem  6697  genpassl  6714  genpassu  6715  ltexprlemell  6788  ltexprlemelu  6789  ltexprlemm  6790  recexprlemell  6812  recexprlemelu  6813  sumeq1  10192  bdsep2  10677  bdzfauscl  10681  strcoll2  10778