Theorem albidv 1954

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

This proof depends on syntax axioms:   → wi 4   ↔ wb 209  ∀wal 1567

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-5 1944

This proof depends on definitions:  df-bi 210

This theorem is used by:  nfbidv  1956  2albidv  1957  sbjust  2099  sbequ  2121  sb6  2123  ax12wdemo  2173  sb4b  2507  mojust  2566  mof  2591  eujust  2599  eujustALT  2600  eu6lem  2601  euf  2604  axextg  2737  axextmo  2739  eqeq1dALT  2766  nfceqdf  2922  drnfc1  2945  drnfc2  2946  ralbidv2  3185  ralxpxfr2d  3603  alexeqg  3608  pm13.183  3623  elab6g  3626  elabd2  3627  eqeu  3667  mo2icl  3675  euind  3685  reuind  3714  cdeqal  3730  sbcal  3801  sbccomlem  3821  sbcabel  3829  csbiebg  3883  ssconb  4081  reldisj  4409  sbcssg  4480  elint  4916  axrep1  5236  axreplem  5237  axrep2  5238  zfrepclf  5247  axsepg  5253  sepg  5254  zfausclOLD  5256  al0ssb  5265  eusv1  5357  euotd  5490  freq1  5622  frsn  5744  iota5  6529  dffun2  6557  sbcfungOLD  6573  funimass4  6960  funcnvmpt  7006  dffo3  7113  dffo3f  7117  eufnfv  7245  dff13  7268  fnssintima  7382  nfriotadw  7395  imaeqalov  7670  tfisi  7880  dfom2  7889  elom  7890  xpord3inddlem  8184  seqomlem2  8475  findcard  9193  findcard2  9194  pssnn  9198  ssfi  9202  findcard3  9288  fiint  9332  elirrv  9604  inf0  9635  axinf2  9654  ttrclss  9734  ttrclselem2  9740  tz9.1  9743  kardenOLD  9973  setrec1lem1  9979  setrec2fun  9986  setrec2lem2  9989  aceq0  10210  dfac5  10220  zfac  10551  brdom3  10620  axpowndlem3  10697  zfcndrep  10712  zfcndac  10717  elgch  10720  engch  10726  axgroth3  10929  axgroth4  10930  elnp  11085  elnpi  11086  infm3  12289  fz1sbc  13747  uzrdgfni  14114  trclfvcotr  15177  relexpindlem  15231  vdwmc2  17172  ramtlecl  17193  ramval  17201  ramub  17206  rami  17208  ramcl  17222  mreexexd  17837  mplsubglem  22321  mpllsslem  22322  ismhp3  22478  istopg  23228  1stccn  23797  iskgen3  23883  fbfinnfr  24175  cnextfun  24398  metcld  25642  metcld2  25643  noseqrdgfn  28707  chlimi  31851  nmcexi  32643  disjxun0  33225  disjrdx  33242  axprALT2  35798  tz9.1regs  35876  axsepg5  35886  elkarden  35897  srepdf  36044  mclsssvlem  36451  mclsval  36452  mclsind  36459  elintfv  36660  dfon2lem6  36680  dfon2lem7  36681  dfon2lem8  36682  dfon2  36684  sscoid  36805  sbequbidv  37133  disjeq12dv  37134  ixpeq12dv  37135  cbvsbdavw  37173  cbvsbdavw2  37174  cbvdisjdavw  37187  cbvdisjdavw2  37208  trer  37234  axtcond  37396  axuntco  37397  regsfromregtco  37456  mh-regprimbi  37463  bj-ssblem1  37683  bj-ax12  37686  mobidvALT  37899  bj-sbceqgALT  37944  bj-inex1gALT  37967  bj-nuliota  38114  bj-bm1.3ii  38121  wl-ax12v2cl  38572  wl-mo2t  38650  findcard4  38775  isass  38923  releccnveq  39336  ecin0  39427  inecmo  39430  alrmomodm  39434  raldmqseu  39440  extssr  39664  eltrrels3  39739  eleqvrels3  39752  axc11n-16  40138  cdlemefrs29bpre0  41596  eu6w  43830  unielss  44363  orddif0suc  44413  elmapintab  44739  cnvcnvintabd  44743  iunrelexpuztr  44862  ntrneiiso  45234  ntrneik2  45235  ntrneix2  45236  ntrneikb  45237  mnuop123d  45389  pm14.122b  45549  iotavalb  45556  trsbc  45665  permaxnul  46140  permaxpow  46141  permaxpr  46142  permaxun  46143  permaxinf2lem  46144  permac8prim  46146  nregmodel  46149  eusnsn  48238  aiota0def  48308  ichbidv  48677  mof0  50091  eufsnlem  50094  termcarweu  50805  setrecseq  51005