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  3589  alexeqg  3594  pm13.183  3609  elab6g  3612  elabd2  3613  eqeu  3653  mo2icl  3661  euind  3671  reuind  3700  cdeqal  3716  sbcal  3789  sbccomlem  3808  sbcabel  3817  csbiebg  3870  ssconb  4083  reldisj  4394  sbcssg  4462  elint  4896  axrep1  5214  axreplem  5215  axrep2  5216  axrep4OLD  5220  zfrepclf  5227  axsepg  5233  zfauscl  5234  bm1.3iiOLD  5238  al0ssb  5244  eusv1  5329  euotd  5462  freq1  5592  frsn  5713  iota5  6476  dffun2  6503  sbcfung  6517  funimass4  6899  funcnvmpt  6944  dffo3  7049  dffo3f  7053  eufnfv  7178  dff13  7203  fnssintima  7311  nfriotadw  7326  imaeqalov  7600  tfisi  7804  dfom2  7813  elom  7814  xpord3inddlem  8098  seqomlem2  8384  findcard  9092  findcard2  9093  pssnn  9097  ssfi  9101  findcard3  9187  fiint  9231  inf0  9536  axinf2  9555  ttrclss  9635  ttrclselem2  9641  tz9.1  9644  karden  9813  aceq0  10034  dfac5  10045  zfac  10376  brdom3  10444  axpowndlem3  10516  zfcndrep  10531  zfcndac  10536  elgch  10539  engch  10545  axgroth3  10748  axgroth4  10749  elnp  10904  elnpi  10905  infm3  12109  fz1sbc  13548  uzrdgfni  13914  trclfvcotr  14965  relexpindlem  15019  vdwmc2  16944  ramtlecl  16965  ramval  16973  ramub  16978  rami  16980  ramcl  16994  mreexexd  17608  mplsubglem  21990  mpllsslem  21991  ismhp3  22121  istopg  22873  1stccn  23441  iskgen3  23527  fbfinnfr  23819  cnextfun  24042  metcld  25286  metcld2  25287  noseqrdgfn  28315  chlimi  31323  nmcexi  32115  disjxun0  32662  disjrdx  32679  axprALT2  35272  tz9.1regs  35297  mclsssvlem  35763  mclsval  35764  mclsind  35771  elintfv  35966  dfon2lem6  35987  dfon2lem7  35988  dfon2lem8  35989  dfon2  35991  sscoid  36112  sbequbidv  36415  disjeq12dv  36416  ixpeq12dv  36417  cbvsbdavw  36455  cbvsbdavw2  36456  cbvdisjdavw  36469  cbvdisjdavw2  36490  trer  36517  axtcond  36679  axuntco  36680  regsfromregtco  36739  mh-regprimbi  36746  bj-ssblem1  36967  bj-ax12  36970  mobidvALT  37183  bj-sbceqgALT  37228  bj-nuliota  37383  bj-bm1.3ii  37390  wl-ax12v2cl  37839  wl-mo2t  37917  isass  38184  releccnveq  38599  ecin0  38690  inecmo  38693  alrmomodm  38697  raldmqseu  38703  extssr  38927  eltrrels3  39002  eleqvrels3  39015  axc11n-16  39401  cdlemefrs29bpre0  40859  eu6w  43126  unielss  43667  orddif0suc  43717  elmapintab  44044  cnvcnvintabd  44048  iunrelexpuztr  44167  ntrneiiso  44539  ntrneik2  44540  ntrneix2  44541  ntrneikb  44542  mnuop123d  44710  pm14.122b  44871  iotavalb  44878  trsbc  44988  permaxnul  45456  permaxpow  45457  permaxpr  45458  permaxun  45459  permaxinf2lem  45460  permac8prim  45462  nregmodel  45465  eusnsn  47489  aiota0def  47559  ichbidv  47928  mof0  49328  eufsnlem  49331  termcarweu  50018  setrecseq  50175  setrec1lem1  50177  setrec2fun  50182  setrec2lem2  50184