Theorem exbidv 1703

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.xps <-> E.xch))

Distinct variable group:   ph,x

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

Proof of Theorem exbidv

Step	Hyp	Ref	Expression
1		ax-17 1416	. 2 |- (ph -> A.xph)
2		albidv.1	. 2 |- (ph -> (ps <-> ch))
3	1, 2	exbidh 1502	1 |- (ph -> (E.xps <-> E.xch))

Syntax hints:   -> wi 4   <-> wb 98  E.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  6507  genpassu  6508  ltexprlemell  6570  ltexprlemelu  6571  ltexprlemm  6572  recexprlemell  6592  recexprlemelu  6593  bdsep2  9274  bdzfauscl  9278  strcoll2  9367