MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  albidv Structured version   Visualization version   GIF version

Theorem albidv 1847
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
StepHypRef Expression
1 ax-5 1837 . 2 (𝜑 → ∀𝑥𝜑)
2 albidv.1 . 2 (𝜑 → (𝜓𝜒))
31, 2albidh 1791 1 (𝜑 → (∀𝑥𝜓 ↔ ∀𝑥𝜒))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 196  wal 1479
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1720  ax-4 1735  ax-5 1837
This theorem depends on definitions:  df-bi 197
This theorem is referenced by:  2albidv  1849  ax12wdemo  2010  eujust  2470  eujustALT  2471  euf  2476  mo2  2477  axext3  2602  axext3ALT  2603  bm1.1  2605  eqeq1dALT  2623  nfceqdf  2758  ralbidv2  2981  ralxpxfr2d  3322  alexeqg  3326  pm13.183  3338  eqeu  3371  mo2icl  3379  euind  3387  reuind  3405  cdeqal  3418  sbcal  3479  sbcabel  3510  csbiebg  3549  ssconb  3735  reldisj  4011  sbcssg  4076  elint  4472  axrep1  4763  axrep2  4764  axrep3  4765  axrep4  4766  zfrepclf  4768  axsep2  4773  zfauscl  4774  bm1.3ii  4775  eusv1  4851  euotd  4965  freq1  5074  frsn  5179  iota5  5859  sbcfung  5900  funimass4  6234  dffo3  6360  eufnfv  6476  dff13  6497  tfisi  7043  dfom2  7052  elom  7053  seqomlem2  7531  pssnn  8163  findcard  8184  findcard2  8185  findcard3  8188  fiint  8222  inf0  8503  axinf2  8522  tz9.1  8590  karden  8743  aceq0  8926  dfac5  8936  zfac  9267  brdom3  9335  axpowndlem3  9406  zfcndrep  9421  zfcndac  9426  elgch  9429  engch  9435  axgroth3  9638  axgroth4  9639  elnp  9794  elnpi  9795  infm3  10967  fz1sbc  12400  uzrdgfni  12740  trclfvcotr  13731  relexpindlem  13784  vdwmc2  15664  ramtlecl  15685  ramval  15693  ramub  15698  rami  15700  ramcl  15714  mreexexd  16289  mreexexdOLD  16290  mplsubglem  19415  mpllsslem  19416  istopg  20681  1stccn  21247  iskgen3  21333  fbfinnfr  21626  cnextfun  21849  metcld  23085  metcld2  23086  chlimi  28061  nmcexi  28855  disjrdx  29376  funcnvmpt  29442  mclsssvlem  31433  mclsval  31434  mclsind  31441  elintfv  31638  dfon2lem6  31667  dfon2lem7  31668  dfon2lem8  31669  dfon2  31671  sscoid  31995  trer  32285  bj-ssbjust  32593  bj-ssbequ  32604  bj-ssblem1  32605  bj-axext3  32744  bj-axrep1  32763  bj-axrep2  32764  bj-axrep3  32765  bj-axrep4  32766  bj-sbceqgALT  32872  bj-axsep2  32896  bj-nuliota  32994  wl-mo2t  33328  isass  33616  axc11n-16  34042  cdlemefrs29bpre0  35503  elmapintab  37721  cnvcnvintabd  37725  iunrelexpuztr  37830  ntrneiiso  38209  ntrneik2  38210  ntrneix2  38211  ntrneikb  38212  pm14.122b  38444  iotavalb  38451  trsbc  38570  sbcalgOLD  38572  dffo3f  39180  fun2dmnopgexmpl  41066  setrecseq  42197  setrec1lem1  42199  setrec2fun  42204  setrec2lem2  42206
  Copyright terms: Public domain W3C validator