Theorem albidv 1778

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

Syntax hints:   -> wi 4   <-> wb 189   A.wal 1453

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

This theorem depends on definitions:  df-bi 190

This theorem is referenced by:  2albidv  1780  ax12wdemo  1920  eujust  2312  eujustALT  2313  euf  2318  mo2  2319  axext3  2444  axext3ALT  2445  bm1.1  2447  eqeq1dALT  2465  nfceqdf  2599  ralbidv2  2835  ralxpxfr2d  3176  alexeqg  3180  pm13.183  3191  eqeu  3221  mo2icl  3229  euind  3237  reuind  3255  cdeqal  3268  sbcal  3329  sbcabel  3357  csbiebg  3398  ssconb  3578  reldisj  3820  sbcssg  3892  elint  4254  axrep1  4530  axrep2  4531  axrep3  4532  axrep4  4533  zfrepclf  4535  axsep2  4540  zfauscl  4541  bm1.3ii  4542  eusv1  4611  euotd  4716  freq1  4823  frsn  4924  iota5  5585  sbcfung  5624  funimass4  5939  dffo3  6060  eufnfv  6164  dff13  6184  tfisi  6712  dfom2  6721  elom  6722  seqomlem2  7194  pssnn  7816  findcard  7836  findcard2  7837  findcard3  7840  fiint  7874  inf0  8152  axinf2  8171  tz9.1  8239  karden  8392  aceq0  8575  dfac5  8585  zfac  8916  brdom3  8982  axpowndlem3  9050  zfcndrep  9065  zfcndac  9070  elgch  9073  engch  9079  axgroth3  9282  axgroth4  9283  elnp  9438  elnpi  9439  infm3  10596  fz1sbc  11899  uzrdgfni  12204  trclfvcotr  13122  relexpindlem  13175  vdwmc2  14978  ramtlecl  15000  ramval  15009  ramvalOLD  15010  ramub  15019  rami  15021  ramcl  15036  mreexexd  15603  mplsubglem  18707  mpllsslem  18708  istopg  19974  1stccn  20527  iskgen3  20613  fbfinnfr  20905  cnextfun  21128  metcld  22324  metcld2  22325  cusgrauvtxb  25273  isass  26093  chlimi  26936  nmcexi  27728  disjrdx  28250  funcnvmpt  28320  mclsssvlem  30249  mclsval  30250  mclsind  30257  dfon2lem6  30483  dfon2lem7  30484  dfon2lem8  30485  dfon2  30487  sscoid  30729  trer  31021  bj-ssbequ  31287  bj-ssblem1  31288  bj-axext3  31429  bj-axrep1  31448  bj-axrep2  31449  bj-axrep3  31450  bj-axrep4  31451  bj-sbceqgALT  31549  bj-axsep2  31573  bj-nuliota  31668  wl-mo2t  31949  axc11n-16  32554  cdlemefrs29bpre0  34008  elmapintab  36247  cnvcnvintabd  36251  iunrelexpuztr  36356  pm14.122b  36818  iotavalb  36825  trsbc  36945  sbcalgOLD  36947  dffo3f  37488  fun2dmnopgexmpl  39070