Theorem albidv 1846

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

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

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1719  ax-4 1734  ax-5 1836

This theorem depends on definitions:  df-bi 197

This theorem is referenced by:  2albidv  1848  ax12wdemo  2009  eujust  2471  eujustALT  2472  euf  2477  mo2  2478  axext3  2603  axext3ALT  2604  bm1.1  2606  eqeq1dALT  2624  nfceqdf  2757  ralbidv2  2980  ralxpxfr2d  3316  alexeqg  3320  pm13.183  3332  eqeu  3364  mo2icl  3372  euind  3380  reuind  3398  cdeqal  3411  sbcal  3472  sbcabel  3503  csbiebg  3542  ssconb  3727  reldisj  3998  sbcssg  4063  elint  4453  axrep1  4742  axrep2  4743  axrep3  4744  axrep4  4745  zfrepclf  4747  axsep2  4752  zfauscl  4753  bm1.3ii  4754  eusv1  4830  euotd  4945  freq1  5054  frsn  5160  iota5  5840  sbcfung  5881  funimass4  6214  dffo3  6340  eufnfv  6456  dff13  6477  tfisi  7020  dfom2  7029  elom  7030  seqomlem2  7506  pssnn  8138  findcard  8159  findcard2  8160  findcard3  8163  fiint  8197  inf0  8478  axinf2  8497  tz9.1  8565  karden  8718  aceq0  8901  dfac5  8911  zfac  9242  brdom3  9310  axpowndlem3  9381  zfcndrep  9396  zfcndac  9401  elgch  9404  engch  9410  axgroth3  9613  axgroth4  9614  elnp  9769  elnpi  9770  infm3  10942  fz1sbc  12373  uzrdgfni  12713  trclfvcotr  13700  relexpindlem  13753  vdwmc2  15626  ramtlecl  15647  ramval  15655  ramub  15660  rami  15662  ramcl  15676  mreexexd  16248  mreexexdOLD  16249  mplsubglem  19374  mpllsslem  19375  istopg  20640  1stccn  21206  iskgen3  21292  fbfinnfr  21585  cnextfun  21808  metcld  23044  metcld2  23045  chlimi  27979  nmcexi  28773  disjrdx  29290  funcnvmpt  29352  mclsssvlem  31220  mclsval  31221  mclsind  31228  dfon2lem6  31447  dfon2lem7  31448  dfon2lem8  31449  dfon2  31451  sscoid  31715  trer  32005  bj-ssbjust  32313  bj-ssbequ  32324  bj-ssblem1  32325  bj-axext3  32465  bj-axrep1  32484  bj-axrep2  32485  bj-axrep3  32486  bj-axrep4  32487  bj-sbceqgALT  32597  bj-axsep2  32621  bj-nuliota  32719  wl-mo2t  33028  isass  33316  axc11n-16  33742  cdlemefrs29bpre0  35203  elmapintab  37422  cnvcnvintabd  37426  iunrelexpuztr  37531  ntrneiiso  37910  ntrneik2  37911  ntrneix2  37912  ntrneikb  37913  pm14.122b  38145  iotavalb  38152  trsbc  38271  sbcalgOLD  38273  dffo3f  38873  fun2dmnopgexmpl  40630  setrecseq  41755  setrec1lem1  41757  setrec2fun  41762  setrec2lem2  41764