Theorem albidv 1721

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 1712	. 2 |- ( ph -> A. x ph )
2		albidv.1	. 2 |- ( ph -> ( ps <-> ch ) )
3	1, 2	albidh 1683	1 |- ( ph -> ( A. x ps <-> A. x ch ) )

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

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1626  ax-4 1639  ax-5 1712

This theorem depends on definitions:  df-bi 185

This theorem is referenced by:  2albidv  1723  ax12wdemo  1839  ax12vOLD  1864  eujust  2220  eujustALT  2221  euf  2228  mo2  2229  axext3  2362  axext3OLD  2363  bm1.1  2365  bm1.1OLD  2366  eqeq1dALT  2385  eqeq1OLD  2387  nfceqdf  2539  ralbidv2  2817  ralxpxfr2d  3149  alexeqg  3153  alexeq  3154  pm13.183  3165  eqeu  3195  mo2icl  3203  euind  3211  reuind  3228  cdeqal  3241  sbcal  3302  sbcabel  3330  csbiebg  3371  ssconb  3551  reldisj  3786  sbcssg  3856  elint  4205  axrep1  4479  axrep2  4480  axrep3  4481  axrep4  4482  zfrepclf  4484  axsep2  4489  zfauscl  4490  bm1.3ii  4491  eusv1  4559  euotd  4662  freq1  4763  frsn  4984  iota5  5480  sbcfung  5519  funimass4  5825  dffo3  5948  eufnfv  6047  dff13  6067  tfisi  6592  dfom2  6601  elom  6602  seqomlem2  7034  pssnn  7654  findcard  7674  findcard2  7675  findcard3  7678  fiint  7712  inf0  7952  axinf2  7971  tz9.1  8073  karden  8226  aceq0  8412  dfac5  8422  zfac  8753  brdom3  8819  axpowndlem3  8887  zfcndrep  8903  zfcndac  8908  elgch  8911  engch  8917  axgroth3  9120  axgroth4  9121  elnp  9276  elnpi  9277  infm3  10418  fz1sbc  11676  uzrdgfni  11972  relexpindlem  12898  vdwmc2  14499  ramtlecl  14520  ramval  14528  ramub  14533  rami  14535  ramcl  14549  mreexexd  15055  mplsubglem  18206  mpllsslem  18207  mplsubglemOLD  18208  mpllsslemOLD  18209  istopg  19489  1stccn  20049  iskgen3  20135  fbfinnfr  20427  cnextfun  20649  metcld  21829  metcld2  21830  cusgrauvtxb  24617  isass  25435  chlimi  26269  nmcexi  27061  disjrdx  27580  funcnvmpt  27656  mclsssvlem  29111  mclsval  29112  mclsind  29119  dfon2lem6  29385  dfon2lem7  29386  dfon2lem8  29387  dfon2  29389  sscoid  29716  wl-mo2t  30185  trer  30300  pm14.122b  31498  iotavalb  31505  trsbc  33647  sbcalgOLD  33649  bj-axext3  34701  bj-axrep1  34721  bj-axrep2  34722  bj-axrep3  34723  bj-axrep4  34724  bj-sbceqgALT  34816  bj-axsep2  34840  bj-nuliota  34934  axc11n-16  35081  cdlemefrs29bpre0  36535  iunrelexpuztr  38224