Theorem albidv 1921

Description: Formula-building rule for universal quantifier (deduction form). See also albidh 1867 and albid 2229. (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  2088  sb6  2090  ax12wdemo  2140  sb4b  2479  mojust  2538  mof  2563  eujust  2571  eujustALT  2572  eu6lem  2573  euf  2576  axextg  2710  axextmo  2712  eqeq1dALT  2739  nfceqdf  2894  drnfc1  2918  drnfc2  2919  ralbidv2  3155  ralxpxfr2d  3600  alexeqg  3605  pm13.183  3620  elab6g  3623  elabd2  3624  eqeu  3664  mo2icl  3672  euind  3682  reuind  3711  cdeqal  3727  sbcal  3800  sbccomlem  3819  sbcabel  3828  csbiebg  3881  ssconb  4094  reldisj  4405  sbcssg  4474  elint  4908  axrep1  5225  axreplem  5226  axrep2  5227  axrep4OLD  5231  zfrepclf  5236  axsepg  5242  zfauscl  5243  bm1.3iiOLD  5247  al0ssb  5253  eusv1  5336  euotd  5461  freq1  5591  frsn  5712  iota5  6475  dffun2  6502  sbcfung  6516  funimass4  6898  dffo3  7047  dffo3f  7051  eufnfv  7175  dff13  7200  fnssintima  7308  nfriotadw  7323  imaeqalov  7597  tfisi  7801  dfom2  7810  elom  7811  xpord3inddlem  8096  seqomlem2  8382  findcard  9090  findcard2  9091  pssnn  9095  ssfi  9099  findcard3  9185  fiint  9229  inf0  9532  axinf2  9551  ttrclss  9631  ttrclselem2  9637  tz9.1  9640  karden  9809  aceq0  10030  dfac5  10041  zfac  10372  brdom3  10440  axpowndlem3  10512  zfcndrep  10527  zfcndac  10532  elgch  10535  engch  10541  axgroth3  10744  axgroth4  10745  elnp  10900  elnpi  10901  infm3  12103  fz1sbc  13518  uzrdgfni  13883  trclfvcotr  14934  relexpindlem  14988  vdwmc2  16909  ramtlecl  16930  ramval  16938  ramub  16943  rami  16945  ramcl  16959  mreexexd  17573  mplsubglem  21956  mpllsslem  21957  ismhp3  22087  istopg  22841  1stccn  23409  iskgen3  23495  fbfinnfr  23787  cnextfun  24010  metcld  25264  metcld2  25265  noseqrdgfn  28304  chlimi  31311  nmcexi  32103  disjxun0  32651  disjrdx  32668  funcnvmpt  32747  tz9.1regs  35292  mclsssvlem  35758  mclsval  35759  mclsind  35766  elintfv  35961  dfon2lem6  35982  dfon2lem7  35983  dfon2lem8  35984  dfon2  35986  sscoid  36107  sbequbidv  36410  disjeq12dv  36411  ixpeq12dv  36412  cbvsbdavw  36450  cbvsbdavw2  36451  cbvdisjdavw  36464  cbvdisjdavw2  36485  trer  36512  regsfromregtr  36670  bj-ssblem1  36857  bj-ax12  36860  mobidvALT  37060  bj-sbceqgALT  37105  bj-nuliota  37260  bj-bm1.3ii  37267  wl-ax12v2cl  37713  wl-mo2t  37782  isass  38049  releccnveq  38459  ecin0  38550  inecmo  38553  alrmomodm  38557  raldmqseu  38563  extssr  38784  eltrrels3  38859  eleqvrels3  38872  axc11n-16  39220  cdlemefrs29bpre0  40678  eu6w  42940  unielss  43481  orddif0suc  43531  elmapintab  43858  cnvcnvintabd  43862  iunrelexpuztr  43981  ntrneiiso  44353  ntrneik2  44354  ntrneix2  44355  ntrneikb  44356  mnuop123d  44524  pm14.122b  44685  iotavalb  44692  trsbc  44802  permaxnul  45270  permaxpow  45271  permaxpr  45272  permaxun  45273  permaxinf2lem  45274  permac8prim  45276  nregmodel  45279  eusnsn  47293  aiota0def  47363  ichbidv  47720  mof0  49104  eufsnlem  49107  termcarweu  49794  setrecseq  49951  setrec1lem1  49953  setrec2fun  49958  setrec2lem2  49960