Theorem albidv 1920

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

Syntax hints:   → wi 4   ↔ wb 206  ∀wal 1538

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910

This theorem depends on definitions:  df-bi 207

This theorem is referenced by:  nfbidv  1922  2albidv  1923  sbjust  2064  sbequ  2084  sb6  2086  ax12wdemo  2136  sb4b  2473  mojust  2532  mof  2556  eujust  2564  eujustALT  2565  eu6lem  2566  euf  2569  axextg  2703  axextmo  2705  eqeq1dALT  2732  nfceqdf  2887  drnfc1  2911  drnfc2  2912  ralbidv2  3152  ralxpxfr2d  3609  alexeqg  3614  pm13.183  3629  elab6g  3632  elabd2  3633  eqeu  3674  mo2icl  3682  euind  3692  reuind  3721  cdeqal  3737  sbcal  3810  sbccomlem  3829  sbcabel  3838  csbiebg  3891  ssconb  4101  reldisj  4412  sbcssg  4479  elint  4912  axrep1  5230  axreplem  5231  axrep2  5232  axrep4OLD  5236  zfrepclf  5241  axsepg  5247  zfauscl  5248  bm1.3iiOLD  5252  al0ssb  5258  eusv1  5341  euotd  5468  freq1  5598  frsn  5719  iota5  6482  dffun2  6509  sbcfung  6524  funimass4  6907  dffo3  7056  dffo3f  7060  eufnfv  7185  dff13  7211  fnssintima  7319  nfriotadw  7334  imaeqalov  7608  tfisi  7815  dfom2  7824  elom  7825  xpord3inddlem  8110  seqomlem2  8396  findcard  9104  findcard2  9105  pssnn  9109  ssfi  9114  findcard3  9205  findcard3OLD  9206  fiint  9253  fiintOLD  9254  inf0  9550  axinf2  9569  ttrclss  9649  ttrclselem2  9655  tz9.1  9658  karden  9824  aceq0  10047  dfac5  10058  zfac  10389  brdom3  10457  axpowndlem3  10528  zfcndrep  10543  zfcndac  10548  elgch  10551  engch  10557  axgroth3  10760  axgroth4  10761  elnp  10916  elnpi  10917  infm3  12118  fz1sbc  13537  uzrdgfni  13899  trclfvcotr  14951  relexpindlem  15005  vdwmc2  16926  ramtlecl  16947  ramval  16955  ramub  16960  rami  16962  ramcl  16976  mreexexd  17589  mplsubglem  21941  mpllsslem  21942  ismhp3  22062  istopg  22815  1stccn  23383  iskgen3  23469  fbfinnfr  23761  cnextfun  23984  metcld  25239  metcld2  25240  noseqrdgfn  28240  chlimi  31213  nmcexi  32005  disjxun0  32553  disjrdx  32570  funcnvmpt  32641  mclsssvlem  35542  mclsval  35543  mclsind  35550  elintfv  35745  dfon2lem6  35769  dfon2lem7  35770  dfon2lem8  35771  dfon2  35773  sscoid  35894  sbequbidv  36195  disjeq12dv  36196  ixpeq12dv  36197  cbvsbdavw  36235  cbvsbdavw2  36236  cbvdisjdavw  36249  cbvdisjdavw2  36270  trer  36297  bj-ssblem1  36635  bj-ax12  36638  mobidvALT  36838  bj-sbceqgALT  36883  bj-nuliota  37038  bj-bm1.3ii  37045  wl-ax12v2cl  37487  wl-mo2t  37556  isass  37833  releccnveq  38240  ecin0  38327  inecmo  38330  alrmomodm  38334  extssr  38493  eltrrels3  38564  eleqvrels3  38577  axc11n-16  38924  cdlemefrs29bpre0  40383  eu6w  42657  unielss  43200  orddif0suc  43250  elmapintab  43578  cnvcnvintabd  43582  iunrelexpuztr  43701  ntrneiiso  44073  ntrneik2  44074  ntrneix2  44075  ntrneikb  44076  mnuop123d  44244  pm14.122b  44405  iotavalb  44412  trsbc  44523  permaxnul  44991  permaxpow  44992  permaxpr  44993  permaxun  44994  permaxinf2lem  44995  permac8prim  44997  nregmodel  45000  eusnsn  47020  aiota0def  47090  ichbidv  47447  mof0  48819  eufsnlem  48822  termcarweu  49510  setrecseq  49667  setrec1lem1  49669  setrec2fun  49674  setrec2lem2  49676