Theorem albidv 1924

Description: Formula-building rule for universal quantifier (deduction form). See also albidh 1870 and albid 2218. (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 1537

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1799  ax-4 1813  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  2133  sb4b  2475  sb4bOLD  2476  mojust  2539  mof  2563  eujust  2571  eujustALT  2572  eu6lem  2573  euf  2576  axextg  2711  axextmo  2713  eqeq1dALT  2741  nfcriOLD  2896  nfceqdf  2901  nfceqdfOLD  2902  drnfc1  2925  drnfc1OLD  2926  drnfc2  2927  drnfc2OLD  2928  ralbidv2  3118  ralxpxfr2d  3568  alexeqg  3573  pm13.183  3590  elab6g  3593  elabd2  3594  eqeu  3636  mo2icl  3644  euind  3654  reuind  3683  cdeqal  3699  sbcal  3776  sbcabel  3807  csbiebg  3861  ssconb  4068  reldisj  4382  reldisjOLD  4383  sbcssg  4451  elint  4882  axrep1  5206  axreplem  5207  axrep2  5208  axrep4  5210  zfrepclf  5213  axsepg  5219  zfauscl  5220  bm1.3ii  5221  al0ssb  5227  eusv1  5309  euotd  5421  freq1  5550  frsn  5665  iota5  6401  sbcfung  6442  funimass4  6816  dffo3  6960  eufnfv  7087  dff13  7109  nfriotadw  7220  tfisi  7680  dfom2  7689  elom  7690  seqomlem2  8252  findcard  8908  findcard2  8909  pssnn  8913  ssfi  8918  pssnnOLD  8969  findcard2OLD  8986  findcard3  8987  fiint  9021  inf0  9309  axinf2  9328  tz9.1  9418  karden  9584  aceq0  9805  dfac5  9815  zfac  10147  brdom3  10215  axpowndlem3  10286  zfcndrep  10301  zfcndac  10306  elgch  10309  engch  10315  axgroth3  10518  axgroth4  10519  elnp  10674  elnpi  10675  infm3  11864  fz1sbc  13261  uzrdgfni  13606  trclfvcotr  14648  relexpindlem  14702  vdwmc2  16608  ramtlecl  16629  ramval  16637  ramub  16642  rami  16644  ramcl  16658  mreexexd  17274  mplsubglem  21115  mpllsslem  21116  ismhp3  21243  istopg  21952  1stccn  22522  iskgen3  22608  fbfinnfr  22900  cnextfun  23123  metcld  24375  metcld2  24376  chlimi  29497  nmcexi  30289  disjxun0  30814  disjrdx  30831  funcnvmpt  30906  mclsssvlem  33424  mclsval  33425  mclsind  33432  fnssintima  33578  elintfv  33644  dfon2lem6  33670  dfon2lem7  33671  dfon2lem8  33672  dfon2  33674  ttrclss  33706  ttrclselem2  33712  xpord3ind  33727  sscoid  34142  trer  34432  bj-ssblem1  34762  bj-ax12  34765  mobidvALT  34968  bj-sbceqgALT  35014  bj-nuliota  35155  bj-bm1.3ii  35162  wl-mo2t  35657  isass  35931  releccnveq  36324  ecin0  36411  inecmo  36414  alrmomodm  36418  extssr  36554  eltrrels3  36621  eleqvrels3  36633  axc11n-16  36879  cdlemefrs29bpre0  38337  elmapintab  41093  cnvcnvintabd  41097  iunrelexpuztr  41216  ntrneiiso  41590  ntrneik2  41591  ntrneix2  41592  ntrneikb  41593  mnuop123d  41769  pm14.122b  41930  iotavalb  41937  trsbc  42049  dffo3f  42606  eusnsn  44407  aiota0def  44475  ichbidv  44793  mof0  46053  eufsnlem  46056  setrecseq  46277  setrec1lem1  46279  setrec2fun  46284  setrec2lem2  46286