Theorem albidv 2014

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 2004	. 2 ⊢ (𝜑 → ∀𝑥𝜑)
2		albidv.1	. 2 ⊢ (𝜑 → (𝜓 ↔ 𝜒))
3	1, 2	albidh 1957	1 ⊢ (𝜑 → (∀𝑥𝜓 ↔ ∀𝑥𝜒))

Syntax hints:   → wi 4   ↔ wb 197  ∀wal 1635

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1880  ax-4 1897  ax-5 2004

This theorem depends on definitions:  df-bi 198

This theorem is referenced by:  2albidv  2016  ax12wdemo  2180  eujust  2634  eujustALT  2635  euf  2640  mo2  2641  axext3  2786  axext3ALT  2787  axextmo  2789  bm1.1OLD  2790  eqeq1dALT  2808  nfceqdf  2943  ralbidv2  3171  ralxpxfr2d  3520  alexeqg  3525  pm13.183  3538  eqeu  3572  mo2icl  3580  euind  3588  reuind  3606  cdeqal  3619  sbcal  3680  sbcabel  3709  csbiebg  3748  ssconb  3939  reldisj  4214  sbcssg  4275  elint  4671  axrep1  4961  axreplem  4962  axrep2  4963  axrep4  4965  zfrepclf  4967  axsep2  4972  zfauscl  4973  bm1.3ii  4974  al0ssb  4982  eusv1  5057  euotd  5165  freq1  5278  frsn  5388  iota5  6081  sbcfung  6122  funimass4  6465  dffo3  6593  eufnfv  6713  dff13  6733  tfisi  7285  dfom2  7294  elom  7295  seqomlem2  7779  pssnn  8414  findcard  8435  findcard2  8436  findcard3  8439  fiint  8473  inf0  8762  axinf2  8781  tz9.1  8849  karden  9002  aceq0  9221  dfac5  9231  zfac  9564  brdom3  9632  axpowndlem3  9703  zfcndrep  9718  zfcndac  9723  elgch  9726  engch  9732  axgroth3  9935  axgroth4  9936  elnp  10091  elnpi  10092  infm3  11264  fz1sbc  12635  uzrdgfni  12977  trclfvcotr  13969  relexpindlem  14022  vdwmc2  15896  ramtlecl  15917  ramval  15925  ramub  15930  rami  15932  ramcl  15946  mreexexd  16509  mplsubglem  19639  mpllsslem  19640  istopg  20909  1stccn  21476  iskgen3  21562  fbfinnfr  21854  cnextfun  22077  metcld  23312  metcld2  23313  chlimi  28416  nmcexi  29210  disjrdx  29726  funcnvmpt  29792  mclsssvlem  31779  mclsval  31780  mclsind  31787  elintfv  31981  dfon2lem6  32010  dfon2lem7  32011  dfon2lem8  32012  dfon2  32014  sscoid  32338  trer  32628  bj-ssbjust  32931  bj-ssbequ  32942  bj-ssblem1  32943  bj-axext3  33080  bj-axrep1  33099  bj-axrep2  33100  bj-axrep3  33101  bj-axrep4  33102  bj-sbceqgALT  33202  bj-axsep2  33228  bj-nuliota  33326  bj-bm1.3ii  33331  wl-mo2t  33668  isass  33953  releccnveq  34337  ecin0  34427  inecmo  34430  alrmomodm  34434  extssr  34569  axc11n-16  34714  cdlemefrs29bpre0  36174  elmapintab  38399  cnvcnvintabd  38403  iunrelexpuztr  38508  ntrneiiso  38886  ntrneik2  38887  ntrneix2  38888  ntrneikb  38889  pm14.122b  39120  iotavalb  39127  trsbc  39245  sbcalgOLD  39247  sbcssOLD  39251  dffo3f  39850  eusnsn  41647  aiota0def  41675  fun2dmnopgexmpl  41871  setrecseq  42997  setrec1lem1  42999  setrec2fun  43004  setrec2lem2  43006