Theorem albidv 1922

Description: Formula-building rule for universal quantifier (deduction form). See also albidh 1868 and albid 2230. (Contributed by NM, 26-May-1993.)

Hypothesis

Ref	Expression
albidv.1	⊢ (𝜑 → (𝜓 ↔ 𝜒))

Assertion

Ref	Expression
albidv	⊢ (𝜑 → (∀𝑥𝜓 ↔ ∀𝑥𝜒))

Distinct variable group:   𝜑,𝑥

Allowed substitution hints:   𝜓(𝑥)   𝜒(𝑥)

Proof of Theorem albidv

Step	Hyp	Ref	Expression
1		ax-5 1912	. 2 ⊢ (𝜑 → ∀𝑥𝜑)
2		albidv.1	. 2 ⊢ (𝜑 → (𝜓 ↔ 𝜒))
3	1, 2	albidh 1868	1 ⊢ (𝜑 → (∀𝑥𝜓 ↔ ∀𝑥𝜒))

Syntax hints:   → wi 4   ↔ wb 206  ∀wal 1540

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912

This theorem depends on definitions:  df-bi 207

This theorem is referenced by:  nfbidv  1924  2albidv  1925  sbjust  2067  sbequ  2089  sb6  2091  ax12wdemo  2141  sb4b  2479  mojust  2538  mof  2563  eujust  2571  eujustALT  2572  eu6lem  2573  euf  2576  axextg  2710  axextmo  2712  eqeq1dALT  2739  nfceqdf  2894  drnfc1  2918  drnfc2  2919  ralbidv2  3156  ralxpxfr2d  3588  alexeqg  3593  pm13.183  3608  elab6g  3611  elabd2  3612  eqeu  3652  mo2icl  3660  euind  3670  reuind  3699  cdeqal  3715  sbcal  3788  sbccomlem  3807  sbcabel  3816  csbiebg  3869  ssconb  4082  reldisj  4393  sbcssg  4461  elint  4895  axrep1  5213  axreplem  5214  axrep2  5215  axrep4OLD  5219  zfrepclf  5226  axsepg  5232  zfauscl  5233  bm1.3iiOLD  5237  al0ssb  5243  eusv1  5333  euotd  5467  freq1  5598  frsn  5719  iota5  6481  dffun2  6508  sbcfung  6522  funimass4  6904  funcnvmpt  6949  dffo3  7054  dffo3f  7058  eufnfv  7184  dff13  7209  fnssintima  7317  nfriotadw  7332  imaeqalov  7606  tfisi  7810  dfom2  7819  elom  7820  xpord3inddlem  8104  seqomlem2  8390  findcard  9098  findcard2  9099  pssnn  9103  ssfi  9107  findcard3  9193  fiint  9237  inf0  9542  axinf2  9561  ttrclss  9641  ttrclselem2  9647  tz9.1  9650  karden  9819  aceq0  10040  dfac5  10051  zfac  10382  brdom3  10450  axpowndlem3  10522  zfcndrep  10537  zfcndac  10542  elgch  10545  engch  10551  axgroth3  10754  axgroth4  10755  elnp  10910  elnpi  10911  infm3  12115  fz1sbc  13554  uzrdgfni  13920  trclfvcotr  14971  relexpindlem  15025  vdwmc2  16950  ramtlecl  16971  ramval  16979  ramub  16984  rami  16986  ramcl  17000  mreexexd  17614  mplsubglem  21977  mpllsslem  21978  ismhp3  22108  istopg  22860  1stccn  23428  iskgen3  23514  fbfinnfr  23806  cnextfun  24029  metcld  25273  metcld2  25274  noseqrdgfn  28298  chlimi  31305  nmcexi  32097  disjxun0  32644  disjrdx  32661  axprALT2  35253  tz9.1regs  35278  mclsssvlem  35744  mclsval  35745  mclsind  35752  elintfv  35947  dfon2lem6  35968  dfon2lem7  35969  dfon2lem8  35970  dfon2  35972  sscoid  36093  sbequbidv  36396  disjeq12dv  36397  ixpeq12dv  36398  cbvsbdavw  36436  cbvsbdavw2  36437  cbvdisjdavw  36450  cbvdisjdavw2  36471  trer  36498  axtcond  36660  axuntco  36661  regsfromregtco  36720  mh-regprimbi  36727  bj-ssblem1  36948  bj-ax12  36951  mobidvALT  37164  bj-sbceqgALT  37209  bj-nuliota  37364  bj-bm1.3ii  37371  wl-ax12v2cl  37822  wl-mo2t  37900  isass  38167  releccnveq  38582  ecin0  38673  inecmo  38676  alrmomodm  38680  raldmqseu  38686  extssr  38910  eltrrels3  38985  eleqvrels3  38998  axc11n-16  39384  cdlemefrs29bpre0  40842  eu6w  43109  unielss  43646  orddif0suc  43696  elmapintab  44023  cnvcnvintabd  44027  iunrelexpuztr  44146  ntrneiiso  44518  ntrneik2  44519  ntrneix2  44520  ntrneikb  44521  mnuop123d  44689  pm14.122b  44850  iotavalb  44857  trsbc  44967  permaxnul  45435  permaxpow  45436  permaxpr  45437  permaxun  45438  permaxinf2lem  45439  permac8prim  45441  nregmodel  45444  eusnsn  47474  aiota0def  47544  ichbidv  47913  mof0  49313  eufsnlem  49316  termcarweu  50003  setrecseq  50160  setrec1lem1  50162  setrec2fun  50167  setrec2lem2  50169