Theorem albidv 1947

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

Syntax hints:   → wi 4   ↔ wb 209  ∀wal 1565

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1822  ax-4 1836  ax-5 1937

This theorem depends on definitions:  df-bi 210

This theorem is referenced by:  nfbidv  1949  2albidv  1950  rename-sb  2096  sbequ  2123  sb6  2125  ax12wdemo  2176  sb4b  2513  mojust  2572  mof  2597  eujust  2605  eujustALT  2606  eu6lem  2607  euf  2610  axextg  2743  axextmo  2745  eqeq1dALT  2772  nfceqdf  2927  drnfc1  2950  drnfc2  2951  ralbidv2  3190  ralxpxfr2d  3614  alexeqg  3619  pm13.183  3634  elab6g  3637  elabd2  3638  eqeu  3678  mo2icl  3686  euind  3696  reuind  3725  cdeqal  3741  sbcal  3812  sbccomlem  3831  sbcabel  3840  csbiebg  3893  ssconb  4104  reldisj  4419  sbcssg  4487  elint  4922  axrep1  5243  axreplem  5244  axrep2  5245  axrep4OLD  5249  zfrepclf  5256  axsepg  5262  zfauscl  5263  bm1.3iiOLD  5267  al0ssb  5273  eusv1  5363  euotd  5497  freq1  5629  frsn  5750  iota5  6520  dffun2  6547  sbcfung  6561  funimass4  6946  funcnvmpt  6992  dffo3  7098  dffo3f  7102  eufnfv  7228  dff13  7253  fnssintima  7361  nfriotadw  7376  imaeqalov  7650  tfisi  7855  dfom2  7864  elom  7865  xpord3inddlem  8150  seqomlem2  8438  findcard  9148  findcard2  9149  pssnn  9153  ssfi  9157  findcard3  9243  fiint  9286  elirrv  9559  inf0  9590  axinf2  9609  ttrclss  9689  ttrclselem2  9695  tz9.1  9698  karden  9881  aceq0  10102  dfac5  10112  zfac  10444  brdom3  10512  axpowndlem3  10584  zfcndrep  10599  zfcndac  10604  elgch  10607  engch  10613  axgroth3  10816  axgroth4  10817  elnp  10972  elnpi  10973  infm3  12174  fz1sbc  13628  uzrdgfni  13994  trclfvcotr  15046  relexpindlem  15100  vdwmc2  17039  ramtlecl  17060  ramval  17068  ramub  17073  rami  17075  ramcl  17089  mreexexd  17704  mplsubglem  22117  mpllsslem  22118  ismhp3  22274  istopg  23021  1stccn  23589  iskgen3  23675  fbfinnfr  23967  cnextfun  24190  metcld  25434  metcld2  25435  noseqrdgfn  28465  chlimi  31527  nmcexi  32319  disjxun0  32860  disjrdx  32877  axprALT2  35446  tz9.1regs  35480  axsepg5  35490  elkarden  35501  mclsssvlem  35987  mclsval  35988  mclsind  35995  elintfv  36190  dfon2lem6  36211  dfon2lem7  36212  dfon2lem8  36213  dfon2  36215  sscoid  36336  sbequbidv  36649  disjeq12dv  36650  ixpeq12dv  36651  cbvsbdavw  36689  cbvsbdavw2  36690  cbvdisjdavw  36703  cbvdisjdavw2  36724  trer  36750  axtcond  36912  axuntco  36913  regsfromregtco  36972  mh-regprimbi  36979  bj-ssblem1  37199  bj-ax12  37202  mobidvALT  37415  bj-sbceqgALT  37460  bj-nuliota  37615  bj-bm1.3ii  37622  wl-ax12v2cl  38074  wl-mo2t  38152  isass  38419  releccnveq  38834  ecin0  38925  inecmo  38928  alrmomodm  38932  raldmqseu  38938  extssr  39162  eltrrels3  39237  eleqvrels3  39250  axc11n-16  39636  cdlemefrs29bpre0  41094  eu6w  43334  unielss  43871  orddif0suc  43921  elmapintab  44248  cnvcnvintabd  44252  iunrelexpuztr  44371  ntrneiiso  44743  ntrneik2  44744  ntrneix2  44745  ntrneikb  44746  mnuop123d  44898  pm14.122b  45059  iotavalb  45066  trsbc  45175  permaxnul  45643  permaxpow  45644  permaxpr  45645  permaxun  45646  permaxinf2lem  45647  permac8prim  45649  nregmodel  45652  eusnsn  47686  aiota0def  47756  ichbidv  48125  mof0  49535  eufsnlem  49538  termcarweu  50225  setrecseq  50382  setrec1lem1  50384  setrec2fun  50389  setrec2lem2  50391