Theorem albidv 1924

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

Syntax hints:   → wi 4   ↔ wb 205  ∀wal 1537

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914

This theorem depends on definitions:  df-bi 206

This theorem is referenced by:  nfbidv  1926  2albidv  1927  sbjust  2067  sbequ  2087  sb6  2089  ax12wdemo  2132  sb4b  2476  sb4bOLD  2477  mojust  2540  mof  2564  eujust  2572  eujustALT  2573  eu6lem  2574  euf  2577  axextg  2712  axextmo  2714  eqeq1dALT  2742  nfcriOLD  2898  nfceqdf  2903  nfceqdfOLD  2904  drnfc1  2927  drnfc1OLD  2928  drnfc2  2929  drnfc2OLD  2930  ralbidv2  3111  ralxpxfr2d  3577  alexeqg  3582  pm13.183  3598  elab6g  3601  elabd2  3602  eqeu  3642  mo2icl  3650  euind  3660  reuind  3689  cdeqal  3705  sbcal  3781  sbcabel  3812  csbiebg  3866  ssconb  4073  reldisj  4386  reldisjOLD  4387  sbcssg  4455  elint  4886  axrep1  5211  axreplem  5212  axrep2  5213  axrep4  5215  zfrepclf  5219  axsepg  5225  zfauscl  5226  bm1.3ii  5227  al0ssb  5233  eusv1  5315  euotd  5428  freq1  5560  frsn  5675  iota5  6420  sbcfung  6465  funimass4  6843  dffo3  6987  eufnfv  7114  dff13  7137  nfriotadw  7249  tfisi  7714  dfom2  7723  elom  7724  seqomlem2  8291  findcard  8955  findcard2  8956  pssnn  8960  ssfi  8965  pssnnOLD  9049  findcard2OLD  9065  findcard3  9066  fiint  9100  inf0  9388  axinf2  9407  ttrclss  9487  ttrclselem2  9493  tz9.1  9496  karden  9662  aceq0  9883  dfac5  9893  zfac  10225  brdom3  10293  axpowndlem3  10364  zfcndrep  10379  zfcndac  10384  elgch  10387  engch  10393  axgroth3  10596  axgroth4  10597  elnp  10752  elnpi  10753  infm3  11943  fz1sbc  13341  uzrdgfni  13687  trclfvcotr  14729  relexpindlem  14783  vdwmc2  16689  ramtlecl  16710  ramval  16718  ramub  16723  rami  16725  ramcl  16739  mreexexd  17366  mplsubglem  21214  mpllsslem  21215  ismhp3  21342  istopg  22053  1stccn  22623  iskgen3  22709  fbfinnfr  23001  cnextfun  23224  metcld  24479  metcld2  24480  chlimi  29605  nmcexi  30397  disjxun0  30922  disjrdx  30939  funcnvmpt  31013  mclsssvlem  33533  mclsval  33534  mclsind  33541  fnssintima  33685  elintfv  33747  dfon2lem6  33773  dfon2lem7  33774  dfon2lem8  33775  dfon2  33777  xpord3ind  33809  sscoid  34224  trer  34514  bj-ssblem1  34844  bj-ax12  34847  mobidvALT  35050  bj-sbceqgALT  35096  bj-nuliota  35237  bj-bm1.3ii  35244  wl-mo2t  35739  isass  36013  releccnveq  36405  ecin0  36491  inecmo  36494  alrmomodm  36498  extssr  36634  eltrrels3  36701  eleqvrels3  36713  axc11n-16  36959  cdlemefrs29bpre0  38417  elmapintab  41211  cnvcnvintabd  41215  iunrelexpuztr  41334  ntrneiiso  41708  ntrneik2  41709  ntrneix2  41710  ntrneikb  41711  mnuop123d  41887  pm14.122b  42048  iotavalb  42055  trsbc  42167  dffo3f  42724  eusnsn  44531  aiota0def  44599  ichbidv  44916  mof0  46176  eufsnlem  46179  setrecseq  46402  setrec1lem1  46404  setrec2fun  46409  setrec2lem2  46411