Theorem albidv 1921

Description: Formula-building rule for universal quantifier (deduction form). See also albidh 1867 and albid 2227. (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  2477  mojust  2536  mof  2561  eujust  2569  eujustALT  2570  eu6lem  2571  euf  2574  axextg  2708  axextmo  2710  eqeq1dALT  2737  nfceqdf  2892  drnfc1  2916  drnfc2  2917  ralbidv2  3153  ralxpxfr2d  3598  alexeqg  3603  pm13.183  3618  elab6g  3621  elabd2  3622  eqeu  3662  mo2icl  3670  euind  3680  reuind  3709  cdeqal  3725  sbcal  3798  sbccomlem  3817  sbcabel  3826  csbiebg  3879  ssconb  4092  reldisj  4403  sbcssg  4472  elint  4906  axrep1  5223  axreplem  5224  axrep2  5225  axrep4OLD  5229  zfrepclf  5234  axsepg  5240  zfauscl  5241  bm1.3iiOLD  5245  al0ssb  5251  eusv1  5334  euotd  5459  freq1  5589  frsn  5710  iota5  6473  dffun2  6500  sbcfung  6514  funimass4  6896  dffo3  7045  dffo3f  7049  eufnfv  7173  dff13  7198  fnssintima  7306  nfriotadw  7321  imaeqalov  7595  tfisi  7799  dfom2  7808  elom  7809  xpord3inddlem  8094  seqomlem2  8380  findcard  9086  findcard2  9087  pssnn  9091  ssfi  9095  findcard3  9181  fiint  9225  inf0  9528  axinf2  9547  ttrclss  9627  ttrclselem2  9633  tz9.1  9636  karden  9805  aceq0  10026  dfac5  10037  zfac  10368  brdom3  10436  axpowndlem3  10508  zfcndrep  10523  zfcndac  10528  elgch  10531  engch  10537  axgroth3  10740  axgroth4  10741  elnp  10896  elnpi  10897  infm3  12099  fz1sbc  13514  uzrdgfni  13879  trclfvcotr  14930  relexpindlem  14984  vdwmc2  16905  ramtlecl  16926  ramval  16934  ramub  16939  rami  16941  ramcl  16955  mreexexd  17569  mplsubglem  21952  mpllsslem  21953  ismhp3  22083  istopg  22837  1stccn  23405  iskgen3  23491  fbfinnfr  23783  cnextfun  24006  metcld  25260  metcld2  25261  noseqrdgfn  28267  chlimi  31258  nmcexi  32050  disjxun0  32598  disjrdx  32615  funcnvmpt  32694  tz9.1regs  35239  mclsssvlem  35705  mclsval  35706  mclsind  35713  elintfv  35908  dfon2lem6  35929  dfon2lem7  35930  dfon2lem8  35931  dfon2  35933  sscoid  36054  sbequbidv  36357  disjeq12dv  36358  ixpeq12dv  36359  cbvsbdavw  36397  cbvsbdavw2  36398  cbvdisjdavw  36411  cbvdisjdavw2  36432  trer  36459  bj-ssblem1  36798  bj-ax12  36801  mobidvALT  37001  bj-sbceqgALT  37046  bj-nuliota  37201  bj-bm1.3ii  37208  wl-ax12v2cl  37650  wl-mo2t  37719  isass  37986  releccnveq  38395  ecin0  38484  inecmo  38487  alrmomodm  38491  extssr  38701  eltrrels3  38776  eleqvrels3  38789  axc11n-16  39137  cdlemefrs29bpre0  40595  eu6w  42861  unielss  43402  orddif0suc  43452  elmapintab  43779  cnvcnvintabd  43783  iunrelexpuztr  43902  ntrneiiso  44274  ntrneik2  44275  ntrneix2  44276  ntrneikb  44277  mnuop123d  44445  pm14.122b  44606  iotavalb  44613  trsbc  44723  permaxnul  45191  permaxpow  45192  permaxpr  45193  permaxun  45194  permaxinf2lem  45195  permac8prim  45197  nregmodel  45200  eusnsn  47214  aiota0def  47284  ichbidv  47641  mof0  49025  eufsnlem  49028  termcarweu  49715  setrecseq  49872  setrec1lem1  49874  setrec2fun  49879  setrec2lem2  49881