Theorem albidv 1924

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

Syntax hints:   → wi 4   ↔ wb 205  ∀wal 1540

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914

This theorem depends on definitions:  df-bi 206

This theorem is referenced by:  nfbidv  1926  2albidv  1927  sbjust  2067  sbequ  2087  sb6  2089  ax12wdemo  2132  sb4b  2475  mojust  2534  mof  2558  eujust  2566  eujustALT  2567  eu6lem  2568  euf  2571  axextg  2706  axextmo  2708  eqeq1dALT  2736  nfcriOLD  2894  nfceqdf  2899  nfceqdfOLD  2900  drnfc1  2923  drnfc1OLD  2924  drnfc2  2925  drnfc2OLD  2926  ralbidv2  3174  ralxpxfr2d  3635  alexeqg  3640  pm13.183  3657  elab6g  3660  elabd2  3661  eqeu  3703  mo2icl  3711  euind  3721  reuind  3750  cdeqal  3766  sbcal  3842  sbcabel  3873  csbiebg  3927  ssconb  4138  reldisj  4452  reldisjOLD  4453  sbcssg  4524  elint  4957  axrep1  5287  axreplem  5288  axrep2  5289  axrep4  5291  zfrepclf  5295  axsepg  5301  zfauscl  5302  bm1.3ii  5303  al0ssb  5309  eusv1  5390  euotd  5514  freq1  5647  frsn  5764  iota5  6527  dffun2  6554  sbcfung  6573  funimass4  6957  dffo3  7104  eufnfv  7231  dff13  7254  fnssintima  7359  nfriotadw  7373  imaeqalov  7646  tfisi  7848  dfom2  7857  elom  7858  xpord3inddlem  8140  seqomlem2  8451  findcard  9163  findcard2  9164  pssnn  9168  ssfi  9173  pssnnOLD  9265  findcard2OLD  9284  findcard3  9285  findcard3OLD  9286  fiint  9324  inf0  9616  axinf2  9635  ttrclss  9715  ttrclselem2  9721  tz9.1  9724  karden  9890  aceq0  10113  dfac5  10123  zfac  10455  brdom3  10523  axpowndlem3  10594  zfcndrep  10609  zfcndac  10614  elgch  10617  engch  10623  axgroth3  10826  axgroth4  10827  elnp  10982  elnpi  10983  infm3  12173  fz1sbc  13577  uzrdgfni  13923  trclfvcotr  14956  relexpindlem  15010  vdwmc2  16912  ramtlecl  16933  ramval  16941  ramub  16946  rami  16948  ramcl  16962  mreexexd  17592  mplsubglem  21558  mpllsslem  21559  ismhp3  21686  istopg  22397  1stccn  22967  iskgen3  23053  fbfinnfr  23345  cnextfun  23568  metcld  24823  metcld2  24824  chlimi  30518  nmcexi  31310  disjxun0  31836  disjrdx  31853  funcnvmpt  31923  mclsssvlem  34584  mclsval  34585  mclsind  34592  elintfv  34767  dfon2lem6  34791  dfon2lem7  34792  dfon2lem8  34793  dfon2  34795  sscoid  34916  trer  35249  bj-ssblem1  35579  bj-ax12  35582  mobidvALT  35784  bj-sbceqgALT  35830  bj-nuliota  35986  bj-bm1.3ii  35993  wl-mo2t  36488  isass  36762  releccnveq  37174  ecin0  37269  inecmo  37272  alrmomodm  37276  extssr  37427  eltrrels3  37498  eleqvrels3  37511  axc11n-16  37856  cdlemefrs29bpre0  39315  unielss  42015  orddif0suc  42066  elmapintab  42395  cnvcnvintabd  42399  iunrelexpuztr  42518  ntrneiiso  42890  ntrneik2  42891  ntrneix2  42892  ntrneikb  42893  mnuop123d  43069  pm14.122b  43230  iotavalb  43237  trsbc  43349  dffo3f  43925  eusnsn  45784  aiota0def  45852  ichbidv  46169  mof0  47552  eufsnlem  47555  setrecseq  47778  setrec1lem1  47780  setrec2fun  47785  setrec2lem2  47787