Theorem albidv 1941

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

Syntax hints:   → wi 4   ↔ wb 208  ∀wal 1559

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1816  ax-4 1830  ax-5 1931

This theorem depends on definitions:  df-bi 209

This theorem is referenced by:  nfbidv  1943  2albidv  1944  rename-sb  2090  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  3182  ralxpxfr2d  3606  alexeqg  3611  pm13.183  3626  elab6g  3629  elabd2  3630  eqeu  3670  mo2icl  3678  euind  3688  reuind  3717  cdeqal  3733  sbcal  3804  sbccomlem  3823  sbcabel  3832  csbiebg  3885  ssconb  4096  reldisj  4408  sbcssg  4476  elint  4912  axrep1  5229  axreplem  5230  axrep2  5231  axrep4OLD  5235  zfrepclf  5242  axsepg  5248  zfauscl  5249  bm1.3iiOLD  5253  al0ssb  5259  eusv1  5349  euotd  5483  freq1  5615  frsn  5736  iota5  6505  dffun2  6532  sbcfung  6546  funimass4  6932  funcnvmpt  6978  dffo3  7084  dffo3f  7088  eufnfv  7214  dff13  7239  fnssintima  7347  nfriotadw  7362  imaeqalov  7636  tfisi  7840  dfom2  7849  elom  7850  xpord3inddlem  8135  seqomlem2  8423  findcard  9133  findcard2  9134  pssnn  9138  ssfi  9142  findcard3  9228  fiint  9272  elirrv  9546  inf0  9577  axinf2  9596  ttrclss  9676  ttrclselem2  9682  tz9.1  9685  karden  9854  aceq0  10075  dfac5  10086  zfac  10418  brdom3  10486  axpowndlem3  10558  zfcndrep  10573  zfcndac  10578  elgch  10581  engch  10587  axgroth3  10790  axgroth4  10791  elnp  10946  elnpi  10947  infm3  12152  fz1sbc  13606  uzrdgfni  13972  trclfvcotr  15023  relexpindlem  15077  vdwmc2  17016  ramtlecl  17037  ramval  17045  ramub  17050  rami  17052  ramcl  17066  mreexexd  17681  mplsubglem  22051  mpllsslem  22052  ismhp3  22208  istopg  22956  1stccn  23524  iskgen3  23610  fbfinnfr  23902  cnextfun  24125  metcld  25369  metcld2  25370  noseqrdgfn  28400  chlimi  31438  nmcexi  32230  disjxun0  32775  disjrdx  32792  axprALT2  35406  tz9.1regs  35431  axsepg5  35441  mclsssvlem  35913  mclsval  35914  mclsind  35921  elintfv  36116  dfon2lem6  36137  dfon2lem7  36138  dfon2lem8  36139  dfon2  36141  sscoid  36262  sbequbidv  36575  disjeq12dv  36576  ixpeq12dv  36577  cbvsbdavw  36615  cbvsbdavw2  36616  cbvdisjdavw  36629  cbvdisjdavw2  36650  trer  36677  axtcond  36839  axuntco  36840  regsfromregtco  36899  mh-regprimbi  36906  bj-ssblem1  37127  bj-ax12  37130  mobidvALT  37343  bj-sbceqgALT  37388  bj-nuliota  37543  bj-bm1.3ii  37550  wl-ax12v2cl  38001  wl-mo2t  38079  isass  38346  releccnveq  38761  ecin0  38852  inecmo  38855  alrmomodm  38859  raldmqseu  38865  extssr  39089  eltrrels3  39164  eleqvrels3  39177  axc11n-16  39563  cdlemefrs29bpre0  41021  eu6w  43259  unielss  43796  orddif0suc  43846  elmapintab  44173  cnvcnvintabd  44177  iunrelexpuztr  44296  ntrneiiso  44668  ntrneik2  44669  ntrneix2  44670  ntrneikb  44671  mnuop123d  44839  pm14.122b  45000  iotavalb  45007  trsbc  45117  permaxnul  45585  permaxpow  45586  permaxpr  45587  permaxun  45588  permaxinf2lem  45589  permac8prim  45591  nregmodel  45594  eusnsn  47621  aiota0def  47691  ichbidv  48060  mof0  49460  eufsnlem  49463  termcarweu  50150  setrecseq  50307  setrec1lem1  50309  setrec2fun  50314  setrec2lem2  50316