Theorem albidv 1915

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

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

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1789  ax-4 1803  ax-5 1905

This theorem depends on definitions:  df-bi 206

This theorem is referenced by:  nfbidv  1917  2albidv  1918  sbjust  2058  sbequ  2078  sb6  2080  ax12wdemo  2123  sb4b  2468  mojust  2527  mof  2551  eujust  2559  eujustALT  2560  eu6lem  2561  euf  2564  axextg  2698  axextmo  2700  eqeq1dALT  2728  nfceqdf  2886  nfceqdfOLD  2887  drnfc1  2911  drnfc1OLD  2912  drnfc2  2913  drnfc2OLD  2914  ralbidv2  3163  ralxpxfr2d  3629  alexeqg  3634  pm13.183  3651  elab6g  3654  elabd2  3655  eqeu  3698  mo2icl  3706  euind  3716  reuind  3745  cdeqal  3761  sbcal  3837  sbcabel  3868  csbiebg  3922  ssconb  4134  reldisj  4453  reldisjOLD  4454  sbcssg  4525  elint  4956  axrep1  5287  axreplem  5288  axrep2  5289  axrep4  5291  zfrepclf  5295  axsepg  5301  zfauscl  5302  bm1.3ii  5303  al0ssb  5309  eusv1  5391  euotd  5515  freq1  5648  frsn  5765  iota5  6532  dffun2  6559  sbcfung  6578  funimass4  6962  dffo3  7111  dffo3f  7115  eufnfv  7241  dff13  7265  fnssintima  7369  nfriotadw  7383  imaeqalov  7660  tfisi  7864  dfom2  7873  elom  7874  xpord3inddlem  8159  seqomlem2  8472  findcard  9188  findcard2  9189  pssnn  9193  ssfi  9198  pssnnOLD  9290  findcard2OLD  9309  findcard3  9310  findcard3OLD  9311  fiint  9350  inf0  9646  axinf2  9665  ttrclss  9745  ttrclselem2  9751  tz9.1  9754  karden  9920  aceq0  10143  dfac5  10153  zfac  10485  brdom3  10553  axpowndlem3  10624  zfcndrep  10639  zfcndac  10644  elgch  10647  engch  10653  axgroth3  10856  axgroth4  10857  elnp  11012  elnpi  11013  infm3  12206  fz1sbc  13612  uzrdgfni  13959  trclfvcotr  14992  relexpindlem  15046  vdwmc2  16951  ramtlecl  16972  ramval  16980  ramub  16985  rami  16987  ramcl  17001  mreexexd  17631  mplsubglem  21961  mpllsslem  21962  ismhp3  22090  istopg  22841  1stccn  23411  iskgen3  23497  fbfinnfr  23789  cnextfun  24012  metcld  25278  metcld2  25279  noseqrdgfn  28229  chlimi  31116  nmcexi  31908  disjxun0  32443  disjrdx  32460  funcnvmpt  32534  mclsssvlem  35303  mclsval  35304  mclsind  35311  elintfv  35491  dfon2lem6  35515  dfon2lem7  35516  dfon2lem8  35517  dfon2  35519  sscoid  35640  trer  35931  bj-ssblem1  36261  bj-ax12  36264  mobidvALT  36465  bj-sbceqgALT  36511  bj-nuliota  36667  bj-bm1.3ii  36674  wl-mo2t  37173  isass  37450  releccnveq  37860  ecin0  37954  inecmo  37957  alrmomodm  37961  extssr  38111  eltrrels3  38182  eleqvrels3  38195  axc11n-16  38540  cdlemefrs29bpre0  39999  eu6w  42236  unielss  42788  orddif0suc  42839  elmapintab  43168  cnvcnvintabd  43172  iunrelexpuztr  43291  ntrneiiso  43663  ntrneik2  43664  ntrneix2  43665  ntrneikb  43666  mnuop123d  43841  pm14.122b  44002  iotavalb  44009  trsbc  44121  eusnsn  46546  aiota0def  46614  ichbidv  46930  mof0  48076  eufsnlem  48079  setrecseq  48302  setrec1lem1  48304  setrec2fun  48309  setrec2lem2  48311