Theorem albidv 1689

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

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

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1601  ax-4 1612  ax-5 1680

This theorem depends on definitions:  df-bi 185

This theorem is referenced by:  2albidv  1691  ax12wdemo  1780  ax12vOLD  1805  sbcom2OLD  2174  axc11n-16  2261  eujust  2277  eujustALT  2278  euf  2285  eufOLD  2286  mo2  2287  moOLD  2327  axext3  2447  axext3OLD  2448  bm1.1  2450  bm1.1OLD  2451  eqeq1dALT  2470  eqeq1OLD  2472  nfceqdf  2624  ralbidv2  2899  ralxpxfr2d  3228  alexeqg  3232  alexeq  3233  pm13.183  3244  eqeu  3274  mo2icl  3282  euind  3290  reuind  3307  cdeqal  3320  sbcal  3383  sbcalgOLD  3384  sbcabel  3420  csbiebg  3458  ssconb  3637  reldisj  3870  sbcssg  3938  elint  4288  axrep1  4559  axrep2  4560  axrep3  4561  axrep4  4562  zfrepclf  4564  axsep2  4569  zfauscl  4570  bm1.3ii  4571  eusv1  4641  euotd  4748  freq1  4849  frsn  5069  iota5  5569  sbcfung  5609  funimass4  5916  dffo3  6034  eufnfv  6132  dff13  6152  tfisi  6671  dfom2  6680  elom  6681  seqomlem2  7113  pssnn  7735  findcard  7755  findcard2  7756  findcard3  7759  fiint  7793  inf0  8034  axinf2  8053  tz9.1  8156  karden  8309  aceq0  8495  dfac5  8505  zfac  8836  brdom3  8902  axpowndlem3  8971  axpowndlem3OLD  8972  zfcndrep  8988  zfcndac  8993  elgch  8996  engch  9002  axgroth3  9205  axgroth4  9206  elnp  9361  elnpi  9362  infm3  10498  fz1sbc  11750  uzrdgfni  12033  vdwmc2  14352  ramtlecl  14373  ramval  14381  ramub  14386  rami  14388  ramcl  14402  mreexexd  14899  mplsubglem  17864  mpllsslem  17865  mplsubglemOLD  17866  mpllsslemOLD  17867  istopg  19171  1stccn  19730  iskgen3  19785  fbfinnfr  20077  cnextfun  20299  metcld  21479  metcld2  21480  cusgrauvtxb  24172  isass  24994  chlimi  25828  nmcexi  26621  disjrdx  27123  funcnvmpt  27182  relexpindlem  28537  dfon2lem6  28797  dfon2lem7  28798  dfon2lem8  28799  dfon2  28801  sscoid  29140  wl-mo2t  29597  trer  29711  pm14.122b  30908  iotavalb  30915  trsbc  32391  bj-axext3  33435  bj-axrep1  33455  bj-axrep2  33456  bj-axrep3  33457  bj-axrep4  33458  bj-sbceqgALT  33550  bj-axsep2  33574  bj-nuliota  33667  cdlemefrs29bpre0  35192