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  30487  nmcexi  31279  disjxun0  31805  disjrdx  31822  funcnvmpt  31892  mclsssvlem  34553  mclsval  34554  mclsind  34561  elintfv  34736  dfon2lem6  34760  dfon2lem7  34761  dfon2lem8  34762  dfon2  34764  sscoid  34885  trer  35201  bj-ssblem1  35531  bj-ax12  35534  mobidvALT  35736  bj-sbceqgALT  35782  bj-nuliota  35938  bj-bm1.3ii  35945  wl-mo2t  36440  isass  36714  releccnveq  37126  ecin0  37221  inecmo  37224  alrmomodm  37228  extssr  37379  eltrrels3  37450  eleqvrels3  37463  axc11n-16  37808  cdlemefrs29bpre0  39267  unielss  41967  orddif0suc  42018  elmapintab  42347  cnvcnvintabd  42351  iunrelexpuztr  42470  ntrneiiso  42842  ntrneik2  42843  ntrneix2  42844  ntrneikb  42845  mnuop123d  43021  pm14.122b  43182  iotavalb  43189  trsbc  43301  dffo3f  43877  eusnsn  45736  aiota0def  45804  ichbidv  46121  mof0  47504  eufsnlem  47507  setrecseq  47730  setrec1lem1  47732  setrec2fun  47737  setrec2lem2  47739