Theorem exbidv 1706

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 1419	. 2 |- ( ph -> A. x ph )
2		albidv.1	. 2 |- ( ph -> ( ps <-> ch ) )
3	1, 2	exbidh 1505	1 |- ( ph -> ( E. x ps <-> E. x ch ) )

Syntax hints:   -> wi 4   <-> wb 98   E.wex 1381

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 1336  ax-gen 1338  ax-ie1 1382  ax-ie2 1383  ax-4 1400  ax-17 1419  ax-ial 1427

This theorem depends on definitions:  df-bi 110

This theorem is referenced by:  ax11ev  1709  2exbidv  1748  3exbidv  1749  eubidh  1906  eubid  1907  eleq1  2100  eleq2  2101  rexbidv2  2329  ceqsex2  2594  alexeq  2670  ceqex  2671  sbc5  2787  sbcex2  2812  sbcexg  2813  sbcabel  2839  eluni  3583  csbunig  3588  intab  3644  cbvopab1  3830  cbvopab1s  3832  axsep2  3876  zfauscl  3877  bnd2  3926  mss  3962  opeqex  3986  euotd  3991  snnex  4181  uniuni  4183  regexmid  4260  reg2exmid  4261  onintexmid  4297  reg3exmid  4304  nnregexmid  4342  opeliunxp  4395  csbxpg  4421  brcog  4502  elrn2g  4525  dfdmf  4528  csbdmg  4529  eldmg  4530  dfrnf  4575  elrn2  4576  elrnmpt1  4585  brcodir  4712  xp11m  4759  xpimasn  4769  csbrng  4782  elxp4  4808  elxp5  4809  dfco2a  4821  cores  4824  funimaexglem  4982  brprcneu  5171  ssimaexg  5235  dmfco  5241  fndmdif  5272  fmptco  5330  fliftf  5439  acexmidlem2  5509  acexmidlemv  5510  cbvoprab1  5576  cbvoprab2  5577  dmtpos  5871  tfrlemi1  5946  ecdmn0m  6148  ereldm  6149  elqsn0m  6174  bren  6228  brdomg  6229  domeng  6233  ac6sfi  6352  ordiso  6358  recexnq  6488  prarloc  6601  genpdflem  6605  genpassl  6622  genpassu  6623  ltexprlemell  6696  ltexprlemelu  6697  ltexprlemm  6698  recexprlemell  6720  recexprlemelu  6721  sumeq1  9874  bdsep2  10006  bdzfauscl  10010  strcoll2  10108