Theorem albidv 1921

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

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

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911

This theorem depends on definitions:  df-bi 209

This theorem is referenced by:  nfbidv  1923  2albidv  1924  sbjust  2068  sbequ  2090  sb6  2093  ax12wdemo  2139  sb4b  2499  sb4bOLD  2500  mojust  2621  mof  2647  eujust  2656  eujustALT  2657  eu6lem  2658  euf  2661  axextg  2795  axextmo  2797  eqeq1dALT  2824  nfceqdf  2972  drnfc1  2997  drnfc2  2999  ralbidv2  3195  ralxpxfr2d  3639  alexeqg  3644  pm13.183  3659  pm13.183OLD  3660  eqeu  3697  mo2icl  3705  euind  3715  reuind  3744  cdeqal  3760  sbcal  3833  sbcabel  3861  csbiebg  3915  ssconb  4114  reldisj  4402  sbcssg  4463  elint  4882  axrep1  5191  axreplem  5192  axrep2  5193  axrep4  5195  zfrepclf  5198  axsepg  5204  zfauscl  5205  bm1.3ii  5206  al0ssb  5212  eusv1  5292  euotd  5403  freq1  5525  frsn  5639  iota5  6338  sbcfung  6379  funimass4  6730  dffo3  6868  eufnfv  6991  dff13  7013  nfriotadw  7122  tfisi  7573  dfom2  7582  elom  7583  seqomlem2  8087  pssnn  8736  findcard  8757  findcard2  8758  findcard3  8761  fiint  8795  inf0  9084  axinf2  9103  tz9.1  9171  karden  9324  aceq0  9544  dfac5  9554  zfac  9882  brdom3  9950  axpowndlem3  10021  zfcndrep  10036  zfcndac  10041  elgch  10044  engch  10050  axgroth3  10253  axgroth4  10254  elnp  10409  elnpi  10410  infm3  11600  fz1sbc  12984  uzrdgfni  13327  trclfvcotr  14369  relexpindlem  14422  vdwmc2  16315  ramtlecl  16336  ramval  16344  ramub  16349  rami  16351  ramcl  16365  mreexexd  16919  mplsubglem  20214  mpllsslem  20215  istopg  21503  1stccn  22071  iskgen3  22157  fbfinnfr  22449  cnextfun  22672  metcld  23909  metcld2  23910  chlimi  29011  nmcexi  29803  disjxun0  30324  disjrdx  30341  funcnvmpt  30412  mclsssvlem  32809  mclsval  32810  mclsind  32817  elintfv  33007  dfon2lem6  33033  dfon2lem7  33034  dfon2lem8  33035  dfon2  33037  sscoid  33374  trer  33664  bj-ssblem1  33987  bj-ax12  33990  mobidvALT  34181  bj-sbceqgALT  34222  bj-nuliota  34353  bj-bm1.3ii  34360  wl-mo2t  34826  wl-dfralf  34854  isass  35139  releccnveq  35534  ecin0  35621  inecmo  35624  alrmomodm  35628  extssr  35764  eltrrels3  35831  eleqvrels3  35843  axc11n-16  36089  cdlemefrs29bpre0  37547  elmapintab  39976  cnvcnvintabd  39980  iunrelexpuztr  40084  ntrneiiso  40461  ntrneik2  40462  ntrneix2  40463  ntrneikb  40464  mnuop123d  40618  pm14.122b  40775  iotavalb  40782  trsbc  40894  dffo3f  41458  eusnsn  43281  aiota0def  43314  setrecseq  44808  setrec1lem1  44810  setrec2fun  44815  setrec2lem2  44817