Theorem albidv 1963

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

Syntax hints:   → wi 4   ↔ wb 198  ∀wal 1599

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1839  ax-4 1853  ax-5 1953

This theorem depends on definitions:  df-bi 199

This theorem is referenced by:  nfbidv  1965  2albidv  1966  ax12wdemo  2129  mojust  2550  mof  2578  mofOLD  2579  eujust  2589  eujustALT  2590  eu6lem  2591  eu6OLD  2594  euf  2595  eufOLD  2596  eubidvOLD  2620  axext3  2756  axext3ALT  2757  axextmo  2759  bm1.1OLD  2760  eqeq1dALT  2781  nfceqdf  2930  drnfc1  2951  drnfc2  2953  ralbidv2  3166  ralxpxfr2d  3530  alexeqg  3535  pm13.183  3549  pm13.183OLD  3550  eqeu  3587  mo2icl  3597  euind  3605  reuind  3628  cdeqal  3641  sbcal  3707  sbcabel  3734  csbiebg  3774  ssconb  3966  reldisj  4245  sbcssg  4306  elint  4716  axrep1  5007  axreplem  5008  axrep2  5009  axrep4  5011  zfrepclf  5013  axsep2  5018  zfauscl  5019  bm1.3ii  5020  al0ssb  5027  eusv1  5103  euotd  5210  freq1  5325  frsn  5437  iota5  6119  sbcfung  6159  funimass4  6507  dffo3  6638  eufnfv  6763  dff13  6784  tfisi  7336  dfom2  7345  elom  7346  seqomlem2  7829  pssnn  8466  findcard  8487  findcard2  8488  findcard3  8491  fiint  8525  inf0  8815  axinf2  8834  tz9.1  8902  karden  9055  aceq0  9274  dfac5  9284  zfac  9617  brdom3  9685  axpowndlem3  9756  zfcndrep  9771  zfcndac  9776  elgch  9779  engch  9785  axgroth3  9988  axgroth4  9989  elnp  10144  elnpi  10145  infm3  11336  fz1sbc  12734  uzrdgfni  13076  trclfvcotr  14157  relexpindlem  14210  vdwmc2  16087  ramtlecl  16108  ramval  16116  ramub  16121  rami  16123  ramcl  16137  mreexexd  16694  mplsubglem  19831  mpllsslem  19832  istopg  21107  1stccn  21675  iskgen3  21761  fbfinnfr  22053  cnextfun  22276  metcld  23512  metcld2  23513  chlimi  28663  nmcexi  29457  disjrdx  29967  funcnvmpt  30032  mclsssvlem  32058  mclsval  32059  mclsind  32066  elintfv  32255  dfon2lem6  32281  dfon2lem7  32282  dfon2lem8  32283  dfon2  32285  sscoid  32609  trer  32899  bj-ssbjustlem  33208  bj-ssbequ  33220  bj-ssblem1  33221  bj-axext3  33346  bj-axrep1  33365  bj-axrep2  33366  bj-axrep3  33367  bj-axrep4  33368  mobidvALT  33414  bj-sbceqgALT  33468  bj-axsep2  33494  bj-nuliota  33591  bj-bm1.3ii  33596  wl-mo2t  33951  wl-dfralf  33976  isass  34269  releccnveq  34657  ecin0  34745  inecmo  34748  alrmomodm  34752  extssr  34887  eltrrels3  34954  eleqvrels3  34965  axc11n-16  35092  cdlemefrs29bpre0  36550  elmapintab  38859  cnvcnvintabd  38863  iunrelexpuztr  38968  ntrneiiso  39345  ntrneik2  39346  ntrneix2  39347  ntrneikb  39348  pm14.122b  39579  iotavalb  39586  trsbc  39700  dffo3f  40287  eusnsn  42095  aiota0def  42124  fun2dmnopgexmpl  42325  setrecseq  43537  setrec1lem1  43539  setrec2fun  43544  setrec2lem2  43546