Theorem albidv 1760

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

Syntax hints:   -> wi 4   <-> wb 187   A.wal 1435

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1665  ax-4 1678  ax-5 1751

This theorem depends on definitions:  df-bi 188

This theorem is referenced by:  2albidv  1762  ax12wdemo  1883  ax12vOLD  1909  eujust  2268  eujustALT  2269  euf  2276  mo2  2277  axext3  2409  axext3OLD  2410  bm1.1  2412  bm1.1OLD  2413  eqeq1dALT  2432  eqeq1OLD  2434  nfceqdf  2586  ralbidv2  2867  ralxpxfr2d  3202  alexeqg  3206  alexeq  3207  pm13.183  3218  eqeu  3248  mo2icl  3256  euind  3264  reuind  3281  cdeqal  3294  sbcal  3355  sbcabel  3383  csbiebg  3424  ssconb  3604  reldisj  3842  sbcssg  3914  elint  4264  axrep1  4539  axrep2  4540  axrep3  4541  axrep4  4542  zfrepclf  4544  axsep2  4549  zfauscl  4550  bm1.3ii  4551  eusv1  4619  euotd  4722  freq1  4824  frsn  4925  iota5  5585  sbcfung  5624  funimass4  5932  dffo3  6052  eufnfv  6154  dff13  6174  tfisi  6699  dfom2  6708  elom  6709  seqomlem2  7176  pssnn  7796  findcard  7816  findcard2  7817  findcard3  7820  fiint  7854  inf0  8126  axinf2  8145  tz9.1  8212  karden  8365  aceq0  8547  dfac5  8557  zfac  8888  brdom3  8954  axpowndlem3  9022  zfcndrep  9038  zfcndac  9043  elgch  9046  engch  9052  axgroth3  9255  axgroth4  9256  elnp  9411  elnpi  9412  infm3  10568  fz1sbc  11868  uzrdgfni  12169  trclfvcotr  13052  relexpindlem  13105  vdwmc2  14892  ramtlecl  14914  ramval  14923  ramvalOLD  14924  ramub  14933  rami  14935  ramcl  14950  mreexexd  15505  mplsubglem  18593  mpllsslem  18594  istopg  19856  1stccn  20409  iskgen3  20495  fbfinnfr  20787  cnextfun  21010  metcld  22168  metcld2  22169  cusgrauvtxb  25069  isass  25889  chlimi  26722  nmcexi  27514  disjrdx  28040  funcnvmpt  28111  mclsssvlem  29988  mclsval  29989  mclsind  29996  dfon2lem6  30221  dfon2lem7  30222  dfon2lem8  30223  dfon2  30225  sscoid  30465  trer  30757  bj-axext3  31134  bj-axrep1  31154  bj-axrep2  31155  bj-axrep3  31156  bj-axrep4  31157  bj-sbceqgALT  31254  bj-axsep2  31278  bj-nuliota  31371  wl-mo2t  31608  axc11n-16  32218  cdlemefrs29bpre0  33672  iunrelexpuztr  35950  pm14.122b  36411  iotavalb  36418  trsbc  36538  sbcalgOLD  36540  dffo3f  37073