Theorem albidv 1849

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

Syntax hints:   -> wi 4   <-> wb 196   A.wal 1481

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1722  ax-4 1737  ax-5 1839

This theorem depends on definitions:  df-bi 197

This theorem is referenced by:  2albidv  1851  ax12wdemo  2012  eujust  2472  eujustALT  2473  euf  2478  mo2  2479  axext3  2604  axext3ALT  2605  bm1.1  2607  eqeq1dALT  2625  nfceqdf  2760  ralbidv2  2984  ralxpxfr2d  3327  alexeqg  3332  pm13.183  3344  eqeu  3377  mo2icl  3385  euind  3393  reuind  3411  cdeqal  3424  sbcal  3485  sbcabel  3517  csbiebg  3556  ssconb  3743  reldisj  4020  sbcssg  4085  elint  4481  axrep1  4772  axrep2  4773  axrep3  4774  axrep4  4775  zfrepclf  4777  axsep2  4782  zfauscl  4783  bm1.3ii  4784  eusv1  4860  euotd  4975  freq1  5084  frsn  5189  iota5  5871  sbcfung  5912  funimass4  6247  dffo3  6374  eufnfv  6491  dff13  6512  tfisi  7058  dfom2  7067  elom  7068  seqomlem2  7546  pssnn  8178  findcard  8199  findcard2  8200  findcard3  8203  fiint  8237  inf0  8518  axinf2  8537  tz9.1  8605  karden  8758  aceq0  8941  dfac5  8951  zfac  9282  brdom3  9350  axpowndlem3  9421  zfcndrep  9436  zfcndac  9441  elgch  9444  engch  9450  axgroth3  9653  axgroth4  9654  elnp  9809  elnpi  9810  infm3  10982  fz1sbc  12416  uzrdgfni  12757  trclfvcotr  13750  relexpindlem  13803  vdwmc2  15683  ramtlecl  15704  ramval  15712  ramub  15717  rami  15719  ramcl  15733  mreexexd  16308  mreexexdOLD  16309  mplsubglem  19434  mpllsslem  19435  istopg  20700  1stccn  21266  iskgen3  21352  fbfinnfr  21645  cnextfun  21868  metcld  23104  metcld2  23105  chlimi  28091  nmcexi  28885  disjrdx  29404  funcnvmpt  29468  mclsssvlem  31459  mclsval  31460  mclsind  31467  elintfv  31662  dfon2lem6  31693  dfon2lem7  31694  dfon2lem8  31695  dfon2  31697  sscoid  32020  trer  32310  bj-ssbjust  32618  bj-ssbequ  32629  bj-ssblem1  32630  bj-axext3  32769  bj-axrep1  32788  bj-axrep2  32789  bj-axrep3  32790  bj-axrep4  32791  bj-sbceqgALT  32897  bj-axsep2  32921  bj-nuliota  33019  wl-mo2t  33357  isass  33645  releccnveq  34022  ecin0  34117  inecmo  34120  alrmomo2  34124  axc11n-16  34223  cdlemefrs29bpre0  35684  elmapintab  37902  cnvcnvintabd  37906  iunrelexpuztr  38011  ntrneiiso  38389  ntrneik2  38390  ntrneix2  38391  ntrneikb  38392  pm14.122b  38624  iotavalb  38631  trsbc  38750  sbcalgOLD  38752  dffo3f  39364  fun2dmnopgexmpl  41303  setrecseq  42432  setrec1lem1  42434  setrec2fun  42439  setrec2lem2  42441