Theorem albidv 1923

Description: Formula-building rule for universal quantifier (deduction form). See also albidh 1869 and albid 2215. (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 1913	. 2 ⊢ (𝜑 → ∀𝑥𝜑)
2		albidv.1	. 2 ⊢ (𝜑 → (𝜓 ↔ 𝜒))
3	1, 2	albidh 1869	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 1797  ax-4 1811  ax-5 1913

This theorem depends on definitions:  df-bi 206

This theorem is referenced by:  nfbidv  1925  2albidv  1926  sbjust  2066  sbequ  2086  sb6  2088  ax12wdemo  2131  sb4b  2474  mojust  2533  mof  2557  eujust  2565  eujustALT  2566  eu6lem  2567  euf  2570  axextg  2705  axextmo  2707  eqeq1dALT  2735  nfcriOLD  2893  nfceqdf  2898  nfceqdfOLD  2899  drnfc1  2922  drnfc1OLD  2923  drnfc2  2924  drnfc2OLD  2925  ralbidv2  3173  ralxpxfr2d  3633  alexeqg  3638  pm13.183  3655  elab6g  3658  elabd2  3659  eqeu  3701  mo2icl  3709  euind  3719  reuind  3748  cdeqal  3764  sbcal  3840  sbcabel  3871  csbiebg  3925  ssconb  4136  reldisj  4450  reldisjOLD  4451  sbcssg  4522  elint  4955  axrep1  5285  axreplem  5286  axrep2  5287  axrep4  5289  zfrepclf  5293  axsepg  5299  zfauscl  5300  bm1.3ii  5301  al0ssb  5307  eusv1  5388  euotd  5512  freq1  5645  frsn  5761  iota5  6523  dffun2  6550  sbcfung  6569  funimass4  6953  dffo3  7100  eufnfv  7227  dff13  7250  fnssintima  7355  nfriotadw  7369  imaeqalov  7642  tfisi  7844  dfom2  7853  elom  7854  xpord3inddlem  8136  seqomlem2  8447  findcard  9159  findcard2  9160  pssnn  9164  ssfi  9169  pssnnOLD  9261  findcard2OLD  9280  findcard3  9281  findcard3OLD  9282  fiint  9320  inf0  9612  axinf2  9631  ttrclss  9711  ttrclselem2  9717  tz9.1  9720  karden  9886  aceq0  10109  dfac5  10119  zfac  10451  brdom3  10519  axpowndlem3  10590  zfcndrep  10605  zfcndac  10610  elgch  10613  engch  10619  axgroth3  10822  axgroth4  10823  elnp  10978  elnpi  10979  infm3  12169  fz1sbc  13573  uzrdgfni  13919  trclfvcotr  14952  relexpindlem  15006  vdwmc2  16908  ramtlecl  16929  ramval  16937  ramub  16942  rami  16944  ramcl  16958  mreexexd  17588  mplsubglem  21549  mpllsslem  21550  ismhp3  21677  istopg  22388  1stccn  22958  iskgen3  23044  fbfinnfr  23336  cnextfun  23559  metcld  24814  metcld2  24815  chlimi  30474  nmcexi  31266  disjxun0  31792  disjrdx  31809  funcnvmpt  31879  mclsssvlem  34541  mclsval  34542  mclsind  34549  elintfv  34724  dfon2lem6  34748  dfon2lem7  34749  dfon2lem8  34750  dfon2  34752  sscoid  34873  trer  35189  bj-ssblem1  35519  bj-ax12  35522  mobidvALT  35724  bj-sbceqgALT  35770  bj-nuliota  35926  bj-bm1.3ii  35933  wl-mo2t  36428  isass  36702  releccnveq  37114  ecin0  37209  inecmo  37212  alrmomodm  37216  extssr  37367  eltrrels3  37438  eleqvrels3  37451  axc11n-16  37796  cdlemefrs29bpre0  39255  unielss  41952  orddif0suc  42003  elmapintab  42332  cnvcnvintabd  42336  iunrelexpuztr  42455  ntrneiiso  42827  ntrneik2  42828  ntrneix2  42829  ntrneikb  42830  mnuop123d  43006  pm14.122b  43167  iotavalb  43174  trsbc  43286  dffo3f  43862  eusnsn  45722  aiota0def  45790  ichbidv  46107  mof0  47457  eufsnlem  47460  setrecseq  47683  setrec1lem1  47685  setrec2fun  47690  setrec2lem2  47692