Theorem albidv 1921

Description: Formula-building rule for universal quantifier (deduction form). See also albidh 1867 and albid 2222. (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 209  ∀wal 1536

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

This theorem depends on definitions:  df-bi 210

This theorem is referenced by:  nfbidv  1923  2albidv  1924  sbjust  2068  sbequ  2088  sb6  2090  ax12wdemo  2136  sb4b  2488  sb4bOLD  2489  mojust  2597  mof  2622  eujust  2631  eujustALT  2632  eu6lem  2633  euf  2636  axextg  2772  axextmo  2774  eqeq1dALT  2801  nfcriOLD  2946  nfceqdf  2951  drnfc1  2974  drnfc2  2975  ralbidv2  3160  ralxpxfr2d  3587  alexeqg  3592  pm13.183  3606  eqeu  3645  mo2icl  3653  euind  3663  reuind  3692  cdeqal  3708  sbcal  3780  sbcabel  3807  csbiebg  3860  ssconb  4065  reldisj  4359  reldisjOLD  4360  sbcssg  4421  elint  4844  axrep1  5155  axreplem  5156  axrep2  5157  axrep4  5159  zfrepclf  5162  axsepg  5168  zfauscl  5169  bm1.3ii  5170  al0ssb  5176  eusv1  5257  euotd  5368  freq1  5489  frsn  5603  iota5  6307  sbcfung  6348  funimass4  6705  dffo3  6845  eufnfv  6969  dff13  6991  nfriotadw  7101  tfisi  7553  dfom2  7562  elom  7563  seqomlem2  8070  pssnn  8720  findcard  8741  findcard2  8742  findcard3  8745  fiint  8779  inf0  9068  axinf2  9087  tz9.1  9155  karden  9308  aceq0  9529  dfac5  9539  zfac  9871  brdom3  9939  axpowndlem3  10010  zfcndrep  10025  zfcndac  10030  elgch  10033  engch  10039  axgroth3  10242  axgroth4  10243  elnp  10398  elnpi  10399  infm3  11587  fz1sbc  12978  uzrdgfni  13321  trclfvcotr  14360  relexpindlem  14414  vdwmc2  16305  ramtlecl  16326  ramval  16334  ramub  16339  rami  16341  ramcl  16355  mreexexd  16911  mplsubglem  20672  mpllsslem  20673  istopg  21500  1stccn  22068  iskgen3  22154  fbfinnfr  22446  cnextfun  22669  metcld  23910  metcld2  23911  chlimi  29017  nmcexi  29809  disjxun0  30337  disjrdx  30354  funcnvmpt  30430  mclsssvlem  32922  mclsval  32923  mclsind  32930  elintfv  33120  dfon2lem6  33146  dfon2lem7  33147  dfon2lem8  33148  dfon2  33150  sscoid  33487  trer  33777  bj-ssblem1  34100  bj-ax12  34103  mobidvALT  34296  bj-sbceqgALT  34343  bj-nuliota  34474  bj-bm1.3ii  34481  wl-mo2t  34976  wl-dfralf  35004  isass  35284  releccnveq  35679  ecin0  35766  inecmo  35769  alrmomodm  35773  extssr  35909  eltrrels3  35976  eleqvrels3  35988  axc11n-16  36234  cdlemefrs29bpre0  37692  elmapintab  40296  cnvcnvintabd  40300  iunrelexpuztr  40420  ntrneiiso  40794  ntrneik2  40795  ntrneix2  40796  ntrneikb  40797  mnuop123d  40970  pm14.122b  41127  iotavalb  41134  trsbc  41246  dffo3f  41806  eusnsn  43618  aiota0def  43651  ichbidv  43970  setrecseq  45215  setrec1lem1  45217  setrec2fun  45222  setrec2lem2  45224