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  2480  mojust  2539  mof  2564  eujust  2572  eujustALT  2573  eu6lem  2574  euf  2577  axextg  2711  axextmo  2713  eqeq1dALT  2740  nfceqdf  2895  drnfc1  2919  drnfc2  2920  ralbidv2  3157  ralxpxfr2d  3602  alexeqg  3607  pm13.183  3622  elab6g  3625  elabd2  3626  eqeu  3666  mo2icl  3674  euind  3684  reuind  3713  cdeqal  3729  sbcal  3802  sbccomlem  3821  sbcabel  3830  csbiebg  3883  ssconb  4096  reldisj  4407  sbcssg  4476  elint  4910  axrep1  5227  axreplem  5228  axrep2  5229  axrep4OLD  5233  zfrepclf  5238  axsepg  5244  zfauscl  5245  bm1.3iiOLD  5249  al0ssb  5255  eusv1  5338  euotd  5469  freq1  5599  frsn  5720  iota5  6483  dffun2  6510  sbcfung  6524  funimass4  6906  funcnvmpt  6951  dffo3  7056  dffo3f  7060  eufnfv  7185  dff13  7210  fnssintima  7318  nfriotadw  7333  imaeqalov  7607  tfisi  7811  dfom2  7820  elom  7821  xpord3inddlem  8106  seqomlem2  8392  findcard  9100  findcard2  9101  pssnn  9105  ssfi  9109  findcard3  9195  fiint  9239  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  12113  fz1sbc  13528  uzrdgfni  13893  trclfvcotr  14944  relexpindlem  14998  vdwmc2  16919  ramtlecl  16940  ramval  16948  ramub  16953  rami  16955  ramcl  16969  mreexexd  17583  mplsubglem  21969  mpllsslem  21970  ismhp3  22100  istopg  22854  1stccn  23422  iskgen3  23508  fbfinnfr  23800  cnextfun  24023  metcld  25277  metcld2  25278  noseqrdgfn  28317  chlimi  31326  nmcexi  32118  disjxun0  32665  disjrdx  32682  axprALT2  35291  tz9.1regs  35316  mclsssvlem  35782  mclsval  35783  mclsind  35790  elintfv  35985  dfon2lem6  36006  dfon2lem7  36007  dfon2lem8  36008  dfon2  36010  sscoid  36131  sbequbidv  36434  disjeq12dv  36435  ixpeq12dv  36436  cbvsbdavw  36474  cbvsbdavw2  36475  cbvdisjdavw  36488  cbvdisjdavw2  36509  trer  36536  regsfromregtr  36694  bj-ssblem1  36903  bj-ax12  36906  mobidvALT  37109  bj-sbceqgALT  37154  bj-nuliota  37309  bj-bm1.3ii  37316  wl-ax12v2cl  37765  wl-mo2t  37834  isass  38101  releccnveq  38516  ecin0  38607  inecmo  38610  alrmomodm  38614  raldmqseu  38620  extssr  38844  eltrrels3  38919  eleqvrels3  38932  axc11n-16  39318  cdlemefrs29bpre0  40776  eu6w  43038  unielss  43579  orddif0suc  43629  elmapintab  43956  cnvcnvintabd  43960  iunrelexpuztr  44079  ntrneiiso  44451  ntrneik2  44452  ntrneix2  44453  ntrneikb  44454  mnuop123d  44622  pm14.122b  44783  iotavalb  44790  trsbc  44900  permaxnul  45368  permaxpow  45369  permaxpr  45370  permaxun  45371  permaxinf2lem  45372  permac8prim  45374  nregmodel  45377  eusnsn  47390  aiota0def  47460  ichbidv  47817  mof0  49201  eufsnlem  49204  termcarweu  49891  setrecseq  50048  setrec1lem1  50050  setrec2fun  50055  setrec2lem2  50057