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  2637  ceqsex2  2895  alexeq  2968  ceqex  2969  sbc2or  3054  sbc5  3070  sbcex2  3095  sbcexg  3096  sbcabel  3123  eluni  3894  csbunig  3899  intab  3956  el1c  4139  opkelopkabg  4245  otkelins3kg  4254  opkelcokg  4261  opkelimagekg  4271  sfineq1  4526  sfineq2  4527  phiall  4618  cbvopab1  4632  cbvopab1s  4634  setconslem6  4736  csbxpg  4813  opeliunxp  4820  br1st  4858  br2nd  4859  brco  4883  dfdmf  4905  dfrnf  4962  csbrng  4966  dfco2a  5081  cores  5084  tz6.12-2  5346  fnrnfv  5364  dmfco  5381  funiunfv  5467  isomin  5496  cbvoprab1  5567  cbvoprab2  5568  oqelins4  5794  txpcofun  5803  erdmrn  5965  mapsn  6026  bren  6030  ce0nnul  6177  ce0ncpw1  6185  dflec3  6221  nclenc  6222  taddc  6229