Theorem exbidv 1626

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

Syntax hints:   -> wi 4   <-> wb 176  E.wex 1541

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1546  ax-5 1557  ax-17 1616

This theorem depends on definitions:  df-bi 177  df-ex 1542

This theorem is referenced by:  2exbidv  1628  3exbidv  1629  eubid  2211  eleq1  2413  eleq2  2414  rexbidv2  2638  ceqsex2  2896  alexeq  2969  ceqex  2970  sbc2or  3055  sbc5  3071  sbcex2  3096  sbcexg  3097  sbcabel  3124  eluni  3895  csbunig  3900  intab  3957  el1c  4140  opkelopkabg  4246  otkelins3kg  4255  opkelcokg  4262  opkelimagekg  4272  sfineq1  4527  sfineq2  4528  phiall  4619  cbvopab1  4633  cbvopab1s  4635  setconslem6  4737  csbxpg  4814  opeliunxp  4821  br1st  4859  br2nd  4860  brco  4884  dfdmf  4906  dfrnf  4963  csbrng  4967  dfco2a  5082  cores  5085  tz6.12-2  5347  fnrnfv  5365  dmfco  5382  funiunfv  5468  isomin  5497  cbvoprab1  5568  cbvoprab2  5569  oqelins4  5795  txpcofun  5804  erdmrn  5966  mapsn  6027  bren  6031  ce0nnul  6178  ce0ncpw1  6186  dflec3  6222  nclenc  6223  taddc  6230