Theorem albidv 1950

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

Syntax hints:   → wi 4   ↔ wb 209  ∀wal 1568

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1825  ax-4 1839  ax-5 1940

This theorem depends on definitions:  df-bi 210

This theorem is referenced by:  nfbidv  1952  2albidv  1953  sbjust  2095  sbequ  2117  sb6  2119  ax12wdemo  2170  sb4b  2507  mojust  2566  mof  2591  eujust  2599  eujustALT  2600  eu6lem  2601  euf  2604  axextg  2737  axextmo  2739  eqeq1dALT  2766  nfceqdf  2921  drnfc1  2944  drnfc2  2945  ralbidv2  3184  ralxpxfr2d  3605  alexeqg  3610  pm13.183  3625  elab6g  3628  elabd2  3629  eqeu  3669  mo2icl  3677  euind  3687  reuind  3716  cdeqal  3732  sbcal  3803  sbccomlem  3822  sbcabel  3831  csbiebg  3885  ssconb  4096  reldisj  4413  sbcssg  4482  elint  4918  axrep1  5239  axreplem  5240  axrep2  5241  axrep4OLD  5245  zfrepclf  5252  axsepg  5258  sepg  5259  zfausclOLD  5261  bm1.3iiOLD  5265  al0ssb  5271  eusv1  5362  euotd  5496  freq1  5628  frsn  5749  iota5  6519  dffun2  6546  sbcfung  6560  funimass4  6945  funcnvmpt  6991  dffo3  7097  dffo3f  7101  eufnfv  7227  dff13  7252  fnssintima  7360  nfriotadw  7375  imaeqalov  7649  tfisi  7851  dfom2  7860  elom  7861  xpord3inddlem  8146  seqomlem2  8434  findcard  9144  findcard2  9145  pssnn  9149  ssfi  9153  findcard3  9239  fiint  9282  elirrv  9555  inf0  9586  axinf2  9605  ttrclss  9685  ttrclselem2  9691  tz9.1  9694  karden  9877  aceq0  10098  dfac5  10108  zfac  10439  brdom3  10507  axpowndlem3  10579  zfcndrep  10594  zfcndac  10599  elgch  10602  engch  10608  axgroth3  10811  axgroth4  10812  elnp  10967  elnpi  10968  infm3  12169  fz1sbc  13624  uzrdgfni  13990  trclfvcotr  15042  relexpindlem  15096  vdwmc2  17034  ramtlecl  17055  ramval  17063  ramub  17068  rami  17070  ramcl  17084  mreexexd  17699  mplsubglem  22148  mpllsslem  22149  ismhp3  22305  istopg  23052  1stccn  23620  iskgen3  23706  fbfinnfr  23998  cnextfun  24221  metcld  25465  metcld2  25466  noseqrdgfn  28499  chlimi  31586  nmcexi  32378  disjxun0  32919  disjrdx  32936  axprALT2  35503  tz9.1regs  35547  axsepg5  35557  elkarden  35568  mclsssvlem  36054  mclsval  36055  mclsind  36062  elintfv  36257  dfon2lem6  36278  dfon2lem7  36279  dfon2lem8  36280  dfon2  36282  sscoid  36403  sbequbidv  36746  disjeq12dv  36747  ixpeq12dv  36748  cbvsbdavw  36786  cbvsbdavw2  36787  cbvdisjdavw  36800  cbvdisjdavw2  36821  trer  36847  axtcond  37009  axuntco  37010  regsfromregtco  37069  mh-regprimbi  37076  bj-ssblem1  37296  bj-ax12  37299  mobidvALT  37512  bj-sbceqgALT  37557  bj-inex1gALT  37580  bj-nuliota  37713  bj-bm1.3ii  37720  wl-ax12v2cl  38172  wl-mo2t  38250  isass  38517  releccnveq  38930  ecin0  39021  inecmo  39024  alrmomodm  39028  raldmqseu  39034  extssr  39258  eltrrels3  39333  eleqvrels3  39346  axc11n-16  39732  cdlemefrs29bpre0  41190  eu6w  43428  unielss  43965  orddif0suc  44015  elmapintab  44342  cnvcnvintabd  44346  iunrelexpuztr  44465  ntrneiiso  44837  ntrneik2  44838  ntrneix2  44839  ntrneikb  44840  mnuop123d  44992  pm14.122b  45153  iotavalb  45160  trsbc  45269  permaxnul  45737  permaxpow  45738  permaxpr  45739  permaxun  45740  permaxinf2lem  45741  permac8prim  45743  nregmodel  45746  eusnsn  47783  aiota0def  47853  ichbidv  48222  mof0  49636  eufsnlem  49639  termcarweu  50326  setrecseq  50483  setrec1lem1  50485  setrec2fun  50490  setrec2lem2  50492