Theorem albidv 1700

Description: Formula-building rule for universal quantifier (deduction rule). (Contributed by NM, 26-May-1993.)

Hypothesis

Ref	Expression
albidv.1	|- ( ph -> ( ps <-> ch ) )

Assertion

Ref	Expression
albidv	|- ( ph -> ( A. x ps <-> A. x ch ) )

Distinct variable group:   ph, x

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

Proof of Theorem albidv

Step	Hyp	Ref	Expression
1		ax-5 1691	. 2 |- ( ph -> A. x ph )
2		albidv.1	. 2 |- ( ph -> ( ps <-> ch ) )
3	1, 2	albidh 1662	1 |- ( ph -> ( A. x ps <-> A. x ch ) )

Syntax hints:   -> wi 4   <-> wb 184   A.wal 1381

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1605  ax-4 1618  ax-5 1691

This theorem depends on definitions:  df-bi 185

This theorem is referenced by:  2albidv  1702  ax12wdemo  1817  ax12vOLD  1842  axc11n-16  2254  eujust  2270  eujustALT  2271  euf  2278  mo2  2279  axext3  2423  axext3OLD  2424  bm1.1  2426  bm1.1OLD  2427  eqeq1dALT  2446  eqeq1OLD  2448  nfceqdf  2600  ralbidv2  2878  ralxpxfr2d  3210  alexeqg  3214  alexeq  3215  pm13.183  3226  eqeu  3256  mo2icl  3264  euind  3272  reuind  3289  cdeqal  3302  sbcal  3365  sbcalgOLD  3366  sbcabel  3402  csbiebg  3443  ssconb  3622  reldisj  3856  sbcssg  3925  elint  4277  axrep1  4549  axrep2  4550  axrep3  4551  axrep4  4552  zfrepclf  4554  axsep2  4559  zfauscl  4560  bm1.3ii  4561  eusv1  4631  euotd  4738  freq1  4839  frsn  5060  iota5  5561  sbcfung  5601  funimass4  5909  dffo3  6031  eufnfv  6131  dff13  6151  tfisi  6678  dfom2  6687  elom  6688  seqomlem2  7118  pssnn  7740  findcard  7761  findcard2  7762  findcard3  7765  fiint  7799  inf0  8041  axinf2  8060  tz9.1  8163  karden  8316  aceq0  8502  dfac5  8512  zfac  8843  brdom3  8909  axpowndlem3  8978  axpowndlem3OLD  8979  zfcndrep  8995  zfcndac  9000  elgch  9003  engch  9009  axgroth3  9212  axgroth4  9213  elnp  9368  elnpi  9369  infm3  10509  fz1sbc  11765  uzrdgfni  12051  vdwmc2  14479  ramtlecl  14500  ramval  14508  ramub  14513  rami  14515  ramcl  14529  mreexexd  15027  mplsubglem  18072  mpllsslem  18073  mplsubglemOLD  18074  mpllsslemOLD  18075  istopg  19382  1stccn  19942  iskgen3  20028  fbfinnfr  20320  cnextfun  20542  metcld  21722  metcld2  21723  cusgrauvtxb  24474  isass  25296  chlimi  26130  nmcexi  26923  disjrdx  27428  funcnvmpt  27488  mclsssvlem  28900  mclsval  28901  mclsind  28908  relexpindlem  29040  dfon2lem6  29196  dfon2lem7  29197  dfon2lem8  29198  dfon2  29200  sscoid  29539  wl-mo2t  29996  trer  30110  pm14.122b  31284  iotavalb  31291  trsbc  33179  bj-axext3  34237  bj-axrep1  34257  bj-axrep2  34258  bj-axrep3  34259  bj-axrep4  34260  bj-sbceqgALT  34352  bj-axsep2  34376  bj-nuliota  34469  cdlemefrs29bpre0  35997