Theorem exbidv 1679

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 1392	. 2 |- (ph -> A.xph)
2		albidv.1	. 2 |- (ph -> (ps <-> ch))
3	1, 2	exbidh 1478	1 |- (ph -> (E.xps <-> E.xch))

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

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 1309  ax-gen 1311  ax-ie1 1355  ax-ie2 1356  ax-4 1373  ax-17 1392  ax-ial 1400

This theorem depends on definitions:  df-bi 110

This theorem is referenced by:  ax11ev  1682  2exbidv  1721  3exbidv  1722  eubidh  1879  eubid  1880  eleq1  2073  eleq2  2074  rexbidv2  2298  ceqsex2  2562  alexeq  2638  ceqex  2639  sbc5  2755  sbcex2  2780  sbcexg  2781  sbcabel  2807  eluni  3546  csbunig  3551  intab  3607  cbvopab1  3793  cbvopab1s  3795  axsep2  3839  zfauscl  3840  bnd2  3889  mss  3925  opeqex  3949  euotd  3954  snnex  4119  uniuni  4121  regexmid  4191  nnregexmid  4257  opeliunxp  4310  csbxpg  4336  brcog  4417  elrn2g  4440  dfdmf  4443  csbdmg  4444  eldmg  4445  dfrnf  4490  elrn2  4491  elrnmpt1  4500  brcodir  4627  xp11m  4674  xpimasn  4684  csbrng  4697  elxp4  4723  elxp5  4724  dfco2a  4736  cores  4739  funimaexglem  4896  brprcneu  5084  ssimaexg  5148  dmfco  5154  fndmdif  5185  fmptco  5243  fliftf  5352  acexmidlem2  5421  acexmidlemv  5422  cbvoprab1  5487  cbvoprab2  5488  dmtpos  5781  tfrlemi1  5855  tfrlemi14  5857  ecdmn0m  6047  ereldm  6048  elqsn0m  6073  recexnq  6235  prarloc  6343  genpdflem  6347  genpassl  6365  genpassu  6366  ltexprlemell  6421  ltexprlemelu  6422  ltexprlemm  6423  recexprlemell  6443  recexprlemelu  6444  bdsep2  8270  bdzfauscl  8274  strcoll2  8363