Theorem albidv 1998

Description: Formula-building rule for universal quantifier (deduction rule). (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 1988	. 2 ⊢ (𝜑 → ∀𝑥𝜑)
2		albidv.1	. 2 ⊢ (𝜑 → (𝜓 ↔ 𝜒))
3	1, 2	albidh 1942	1 ⊢ (𝜑 → (∀𝑥𝜓 ↔ ∀𝑥𝜒))

Syntax hints:   → wi 4   ↔ wb 196  ∀wal 1630

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1871  ax-4 1886  ax-5 1988

This theorem depends on definitions:  df-bi 197

This theorem is referenced by:  2albidv  2000  ax12wdemo  2161  eujust  2609  eujustALT  2610  euf  2615  mo2  2616  axext3  2742  axext3ALT  2743  bm1.1  2745  eqeq1dALT  2763  nfceqdf  2898  ralbidv2  3122  ralxpxfr2d  3466  alexeqg  3471  pm13.183  3484  eqeu  3518  mo2icl  3526  euind  3534  reuind  3552  cdeqal  3565  sbcal  3626  sbcabel  3658  csbiebg  3697  ssconb  3886  reldisj  4163  sbcssg  4229  elint  4633  axrep1  4924  axrep2  4925  axrep3  4926  axrep4  4927  zfrepclf  4929  axsep2  4934  zfauscl  4935  bm1.3ii  4936  eusv1  5009  euotd  5123  freq1  5236  frsn  5346  iota5  6032  sbcfung  6073  funimass4  6410  dffo3  6538  eufnfv  6655  dff13  6676  tfisi  7224  dfom2  7233  elom  7234  seqomlem2  7716  pssnn  8345  findcard  8366  findcard2  8367  findcard3  8370  fiint  8404  inf0  8693  axinf2  8712  tz9.1  8780  karden  8933  aceq0  9151  dfac5  9161  zfac  9494  brdom3  9562  axpowndlem3  9633  zfcndrep  9648  zfcndac  9653  elgch  9656  engch  9662  axgroth3  9865  axgroth4  9866  elnp  10021  elnpi  10022  infm3  11194  fz1sbc  12629  uzrdgfni  12971  trclfvcotr  13969  relexpindlem  14022  vdwmc2  15905  ramtlecl  15926  ramval  15934  ramub  15939  rami  15941  ramcl  15955  mreexexd  16530  mplsubglem  19656  mpllsslem  19657  istopg  20922  1stccn  21488  iskgen3  21574  fbfinnfr  21866  cnextfun  22089  metcld  23324  metcld2  23325  chlimi  28421  nmcexi  29215  disjrdx  29732  funcnvmpt  29798  mclsssvlem  31787  mclsval  31788  mclsind  31795  elintfv  31990  dfon2lem6  32019  dfon2lem7  32020  dfon2lem8  32021  dfon2  32023  sscoid  32347  trer  32637  bj-ssbjust  32946  bj-ssbequ  32957  bj-ssblem1  32958  bj-axext3  33097  bj-axrep1  33116  bj-axrep2  33117  bj-axrep3  33118  bj-axrep4  33119  bj-sbceqgALT  33219  bj-axsep2  33245  bj-nuliota  33343  wl-mo2t  33688  isass  33976  releccnveq  34364  ecin0  34458  inecmo  34461  alrmomodm  34465  extssr  34600  axc11n-16  34745  cdlemefrs29bpre0  36204  elmapintab  38422  cnvcnvintabd  38426  iunrelexpuztr  38531  ntrneiiso  38909  ntrneik2  38910  ntrneix2  38911  ntrneikb  38912  pm14.122b  39144  iotavalb  39151  trsbc  39270  sbcalgOLD  39272  sbcssOLD  39276  dffo3f  39881  fun2dmnopgexmpl  41829  setrecseq  42960  setrec1lem1  42962  setrec2fun  42967  setrec2lem2  42969