Theorem albidv 1927

Description: Formula-building rule for universal quantifier (deduction form). See also albidh 1873 and albid 2234. (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 1917	. 2 ⊢ (𝜑 → ∀𝑥𝜑)
2		albidv.1	. 2 ⊢ (𝜑 → (𝜓 ↔ 𝜒))
3	1, 2	albidh 1873	1 ⊢ (𝜑 → (∀𝑥𝜓 ↔ ∀𝑥𝜒))

Syntax hints:   → wi 4   ↔ wb 207  ∀wal 1545

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917

This theorem depends on definitions:  df-bi 208

This theorem is referenced by:  nfbidv  1929  2albidv  1930  sbjust  2072  sbequ  2094  sb6  2096  ax12wdemo  2146  sb4b  2483  mojust  2542  mof  2567  eujust  2575  eujustALT  2576  eu6lem  2577  euf  2580  axextg  2713  axextmo  2715  eqeq1dALT  2742  nfceqdf  2897  drnfc1  2920  drnfc2  2921  ralbidv2  3158  ralxpxfr2d  3584  alexeqg  3589  pm13.183  3604  elab6g  3607  elabd2  3608  eqeu  3647  mo2icl  3655  euind  3665  reuind  3694  cdeqal  3710  sbcal  3782  sbccomlem  3801  sbcabel  3810  csbiebg  3863  ssconb  4072  reldisj  4381  sbcssg  4449  elint  4883  axrep1  5200  axreplem  5201  axrep2  5202  axrep4OLD  5206  zfrepclf  5213  axsepg  5219  zfauscl  5220  bm1.3iiOLD  5224  al0ssb  5230  eusv1  5320  euotd  5454  freq1  5585  frsn  5706  iota5  6468  dffun2  6495  sbcfung  6509  funimass4  6891  funcnvmpt  6937  dffo3  7043  dffo3f  7047  eufnfv  7173  dff13  7198  fnssintima  7306  nfriotadw  7321  imaeqalov  7595  tfisi  7799  dfom2  7808  elom  7809  xpord3inddlem  8094  seqomlem2  8380  findcard  9088  findcard2  9089  pssnn  9093  ssfi  9097  findcard3  9183  fiint  9227  elirrv  9502  inf0  9533  axinf2  9552  ttrclss  9632  ttrclselem2  9638  tz9.1  9641  karden  9810  aceq0  10031  dfac5  10042  zfac  10373  brdom3  10441  axpowndlem3  10513  zfcndrep  10528  zfcndac  10533  elgch  10536  engch  10542  axgroth3  10745  axgroth4  10746  elnp  10901  elnpi  10902  infm3  12106  fz1sbc  13545  uzrdgfni  13911  trclfvcotr  14962  relexpindlem  15016  vdwmc2  16941  ramtlecl  16962  ramval  16970  ramub  16975  rami  16977  ramcl  16991  mreexexd  17605  mplsubglem  21973  mpllsslem  21974  ismhp3  22130  istopg  22878  1stccn  23446  iskgen3  23532  fbfinnfr  23824  cnextfun  24047  metcld  25291  metcld2  25292  noseqrdgfn  28316  chlimi  31323  nmcexi  32115  disjxun0  32663  disjrdx  32680  axprALT2  35290  tz9.1regs  35315  axsepg5  35325  mclsssvlem  35790  mclsval  35791  mclsind  35798  elintfv  35993  dfon2lem6  36014  dfon2lem7  36015  dfon2lem8  36016  dfon2  36018  sscoid  36139  sbequbidv  36442  disjeq12dv  36443  ixpeq12dv  36444  cbvsbdavw  36482  cbvsbdavw2  36483  cbvdisjdavw  36496  cbvdisjdavw2  36517  trer  36544  axtcond  36706  axuntco  36707  regsfromregtco  36766  mh-regprimbi  36773  bj-ssblem1  36994  bj-ax12  36997  mobidvALT  37210  bj-sbceqgALT  37255  bj-nuliota  37410  bj-bm1.3ii  37417  wl-ax12v2cl  37868  wl-mo2t  37946  isass  38213  releccnveq  38628  ecin0  38719  inecmo  38722  alrmomodm  38726  raldmqseu  38732  extssr  38956  eltrrels3  39031  eleqvrels3  39044  axc11n-16  39430  cdlemefrs29bpre0  40888  eu6w  43126  unielss  43663  orddif0suc  43713  elmapintab  44040  cnvcnvintabd  44044  iunrelexpuztr  44163  ntrneiiso  44535  ntrneik2  44536  ntrneix2  44537  ntrneikb  44538  mnuop123d  44706  pm14.122b  44867  iotavalb  44874  trsbc  44984  permaxnul  45452  permaxpow  45453  permaxpr  45454  permaxun  45455  permaxinf2lem  45456  permac8prim  45458  nregmodel  45461  eusnsn  47489  aiota0def  47559  ichbidv  47928  mof0  49328  eufsnlem  49331  termcarweu  50018  setrecseq  50175  setrec1lem1  50177  setrec2fun  50182  setrec2lem2  50184