Theorem albidv 1921

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

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

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911

This theorem depends on definitions:  df-bi 207

This theorem is referenced by:  nfbidv  1923  2albidv  1924  sbjust  2066  sbequ  2086  sb6  2088  ax12wdemo  2138  sb4b  2475  mojust  2534  mof  2558  eujust  2566  eujustALT  2567  eu6lem  2568  euf  2571  axextg  2705  axextmo  2707  eqeq1dALT  2734  nfceqdf  2890  drnfc1  2914  drnfc2  2915  ralbidv2  3151  ralxpxfr2d  3596  alexeqg  3601  pm13.183  3616  elab6g  3619  elabd2  3620  eqeu  3660  mo2icl  3668  euind  3678  reuind  3707  cdeqal  3723  sbcal  3796  sbccomlem  3815  sbcabel  3824  csbiebg  3877  ssconb  4089  reldisj  4400  sbcssg  4467  elint  4901  axrep1  5216  axreplem  5217  axrep2  5218  axrep4OLD  5222  zfrepclf  5227  axsepg  5233  zfauscl  5234  bm1.3iiOLD  5238  al0ssb  5244  eusv1  5327  euotd  5451  freq1  5581  frsn  5702  iota5  6464  dffun2  6491  sbcfung  6505  funimass4  6886  dffo3  7035  dffo3f  7039  eufnfv  7163  dff13  7188  fnssintima  7296  nfriotadw  7311  imaeqalov  7585  tfisi  7789  dfom2  7798  elom  7799  xpord3inddlem  8084  seqomlem2  8370  findcard  9073  findcard2  9074  pssnn  9078  ssfi  9082  findcard3  9167  fiint  9211  inf0  9511  axinf2  9530  ttrclss  9610  ttrclselem2  9616  tz9.1  9619  karden  9788  aceq0  10009  dfac5  10020  zfac  10351  brdom3  10419  axpowndlem3  10490  zfcndrep  10505  zfcndac  10510  elgch  10513  engch  10519  axgroth3  10722  axgroth4  10723  elnp  10878  elnpi  10879  infm3  12081  fz1sbc  13500  uzrdgfni  13865  trclfvcotr  14916  relexpindlem  14970  vdwmc2  16891  ramtlecl  16912  ramval  16920  ramub  16925  rami  16927  ramcl  16941  mreexexd  17554  mplsubglem  21936  mpllsslem  21937  ismhp3  22057  istopg  22810  1stccn  23378  iskgen3  23464  fbfinnfr  23756  cnextfun  23979  metcld  25233  metcld2  25234  noseqrdgfn  28236  chlimi  31214  nmcexi  32006  disjxun0  32554  disjrdx  32571  funcnvmpt  32649  tz9.1regs  35130  mclsssvlem  35606  mclsval  35607  mclsind  35614  elintfv  35809  dfon2lem6  35830  dfon2lem7  35831  dfon2lem8  35832  dfon2  35834  sscoid  35955  sbequbidv  36258  disjeq12dv  36259  ixpeq12dv  36260  cbvsbdavw  36298  cbvsbdavw2  36299  cbvdisjdavw  36312  cbvdisjdavw2  36333  trer  36360  bj-ssblem1  36698  bj-ax12  36701  mobidvALT  36901  bj-sbceqgALT  36946  bj-nuliota  37101  bj-bm1.3ii  37108  wl-ax12v2cl  37550  wl-mo2t  37619  isass  37896  releccnveq  38305  ecin0  38394  inecmo  38397  alrmomodm  38401  extssr  38611  eltrrels3  38686  eleqvrels3  38699  axc11n-16  39047  cdlemefrs29bpre0  40505  eu6w  42779  unielss  43321  orddif0suc  43371  elmapintab  43699  cnvcnvintabd  43703  iunrelexpuztr  43822  ntrneiiso  44194  ntrneik2  44195  ntrneix2  44196  ntrneikb  44197  mnuop123d  44365  pm14.122b  44526  iotavalb  44533  trsbc  44643  permaxnul  45111  permaxpow  45112  permaxpr  45113  permaxun  45114  permaxinf2lem  45115  permac8prim  45117  nregmodel  45120  eusnsn  47136  aiota0def  47206  ichbidv  47563  mof0  48948  eufsnlem  48951  termcarweu  49639  setrecseq  49796  setrec1lem1  49798  setrec2fun  49803  setrec2lem2  49805