Theorem albidv 1836

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

Syntax hints:   → wi 4   ↔ wb 195  ∀wal 1473

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1713  ax-4 1728  ax-5 1827

This theorem depends on definitions:  df-bi 196

This theorem is referenced by:  2albidv  1838  ax12wdemo  1999  eujust  2460  eujustALT  2461  euf  2466  mo2  2467  axext3  2592  axext3ALT  2593  bm1.1  2595  eqeq1dALT  2613  nfceqdf  2747  ralbidv2  2967  ralxpxfr2d  3298  alexeqg  3302  pm13.183  3313  eqeu  3344  mo2icl  3352  euind  3360  reuind  3378  cdeqal  3391  sbcal  3452  sbcabel  3483  csbiebg  3522  ssconb  3705  reldisj  3972  sbcssg  4035  elint  4416  axrep1  4700  axrep2  4701  axrep3  4702  axrep4  4703  zfrepclf  4705  axsep2  4710  zfauscl  4711  bm1.3ii  4712  eusv1  4786  euotd  4900  freq1  5008  frsn  5112  iota5  5788  sbcfung  5827  funimass4  6157  dffo3  6282  eufnfv  6395  dff13  6416  tfisi  6950  dfom2  6959  elom  6960  seqomlem2  7433  pssnn  8063  findcard  8084  findcard2  8085  findcard3  8088  fiint  8122  inf0  8401  axinf2  8420  tz9.1  8488  karden  8641  aceq0  8824  dfac5  8834  zfac  9165  brdom3  9231  axpowndlem3  9300  zfcndrep  9315  zfcndac  9320  elgch  9323  engch  9329  axgroth3  9532  axgroth4  9533  elnp  9688  elnpi  9689  infm3  10861  fz1sbc  12285  uzrdgfni  12619  trclfvcotr  13598  relexpindlem  13651  vdwmc2  15521  ramtlecl  15542  ramval  15550  ramub  15555  rami  15557  ramcl  15571  mreexexd  16131  mreexexdOLD  16132  mplsubglem  19255  mpllsslem  19256  istopg  20525  1stccn  21076  iskgen3  21162  fbfinnfr  21455  cnextfun  21678  metcld  22912  metcld2  22913  cusgrauvtxb  26024  chlimi  27475  nmcexi  28269  disjrdx  28786  funcnvmpt  28851  mclsssvlem  30713  mclsval  30714  mclsind  30721  dfon2lem6  30937  dfon2lem7  30938  dfon2lem8  30939  dfon2  30941  sscoid  31190  trer  31480  bj-ssbequ  31818  bj-ssblem1  31819  bj-axext3  31957  bj-axrep1  31976  bj-axrep2  31977  bj-axrep3  31978  bj-axrep4  31979  bj-sbceqgALT  32089  bj-axsep2  32113  bj-nuliota  32210  wl-mo2t  32536  isass  32815  axc11n-16  33241  cdlemefrs29bpre0  34702  elmapintab  36921  cnvcnvintabd  36925  iunrelexpuztr  37030  ntrneiiso  37409  ntrneik2  37410  ntrneix2  37411  ntrneikb  37412  pm14.122b  37646  iotavalb  37653  trsbc  37771  sbcalgOLD  37773  dffo3f  38359  fun2dmnopgexmpl  40329  setrecseq  42231  setrec1lem1  42233  setrec2fun  42238  setrec2lem2  42240