Theorem albidv 1926

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

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

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1801  ax-4 1815  ax-5 1916

This theorem depends on definitions:  df-bi 206

This theorem is referenced by:  nfbidv  1928  2albidv  1929  sbjust  2069  sbequ  2089  sb6  2091  ax12wdemo  2134  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  3120  ralxpxfr2d  3576  alexeqg  3581  pm13.183  3598  elab6g  3601  elabd2  3602  eqeu  3644  mo2icl  3652  euind  3662  reuind  3691  cdeqal  3707  sbcal  3784  sbcabel  3815  csbiebg  3869  ssconb  4076  reldisj  4390  reldisjOLD  4391  sbcssg  4459  elint  4890  axrep1  5214  axreplem  5215  axrep2  5216  axrep4  5218  zfrepclf  5221  axsepg  5227  zfauscl  5228  bm1.3ii  5229  al0ssb  5235  eusv1  5317  euotd  5429  freq1  5558  frsn  5673  iota5  6413  sbcfung  6454  funimass4  6828  dffo3  6972  eufnfv  7099  dff13  7122  nfriotadw  7233  tfisi  7693  dfom2  7702  elom  7703  seqomlem2  8266  findcard  8911  findcard2  8912  pssnn  8916  ssfi  8921  pssnnOLD  9001  findcard2OLD  9017  findcard3  9018  fiint  9052  inf0  9340  axinf2  9359  ttrclss  9439  ttrclselem2  9445  tz9.1  9470  karden  9637  aceq0  9858  dfac5  9868  zfac  10200  brdom3  10268  axpowndlem3  10339  zfcndrep  10354  zfcndac  10359  elgch  10362  engch  10368  axgroth3  10571  axgroth4  10572  elnp  10727  elnpi  10728  infm3  11917  fz1sbc  13314  uzrdgfni  13659  trclfvcotr  14701  relexpindlem  14755  vdwmc2  16661  ramtlecl  16682  ramval  16690  ramub  16695  rami  16697  ramcl  16711  mreexexd  17338  mplsubglem  21186  mpllsslem  21187  ismhp3  21314  istopg  22025  1stccn  22595  iskgen3  22681  fbfinnfr  22973  cnextfun  23196  metcld  24451  metcld2  24452  chlimi  29575  nmcexi  30367  disjxun0  30892  disjrdx  30909  funcnvmpt  30983  mclsssvlem  33503  mclsval  33504  mclsind  33511  fnssintima  33655  elintfv  33717  dfon2lem6  33743  dfon2lem7  33744  dfon2lem8  33745  dfon2  33747  xpord3ind  33779  sscoid  34194  trer  34484  bj-ssblem1  34814  bj-ax12  34817  mobidvALT  35020  bj-sbceqgALT  35066  bj-nuliota  35207  bj-bm1.3ii  35214  wl-mo2t  35709  isass  35983  releccnveq  36376  ecin0  36463  inecmo  36466  alrmomodm  36470  extssr  36606  eltrrels3  36673  eleqvrels3  36685  axc11n-16  36931  cdlemefrs29bpre0  38389  elmapintab  41157  cnvcnvintabd  41161  iunrelexpuztr  41280  ntrneiiso  41654  ntrneik2  41655  ntrneix2  41656  ntrneikb  41657  mnuop123d  41833  pm14.122b  41994  iotavalb  42001  trsbc  42113  dffo3f  42670  eusnsn  44471  aiota0def  44539  ichbidv  44857  mof0  46117  eufsnlem  46120  setrecseq  46343  setrec1lem1  46345  setrec2fun  46350  setrec2lem2  46352