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

Theorem albidv 1834
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 1825 . 2 (𝜑 → ∀𝑥𝜑)
2 albidv.1 . 2 (𝜑 → (𝜓𝜒))
31, 2albidh 1778 1 (𝜑 → (∀𝑥𝜓 ↔ ∀𝑥𝜒))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 194  wal 1472
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1711  ax-4 1726  ax-5 1825
This theorem depends on definitions:  df-bi 195
This theorem is referenced by:  2albidv  1836  ax12wdemo  1997  eujust  2455  eujustALT  2456  euf  2461  mo2  2462  axext3  2587  axext3ALT  2588  bm1.1  2590  eqeq1dALT  2608  nfceqdf  2742  ralbidv2  2962  ralxpxfr2d  3293  alexeqg  3297  pm13.183  3308  eqeu  3339  mo2icl  3347  euind  3355  reuind  3373  cdeqal  3386  sbcal  3447  sbcabel  3478  csbiebg  3517  ssconb  3700  reldisj  3967  sbcssg  4030  elint  4406  axrep1  4690  axrep2  4691  axrep3  4692  axrep4  4693  zfrepclf  4695  axsep2  4700  zfauscl  4701  bm1.3ii  4702  eusv1  4777  euotd  4887  freq1  4994  frsn  5098  iota5  5770  sbcfung  5809  funimass4  6138  dffo3  6263  eufnfv  6369  dff13  6390  tfisi  6923  dfom2  6932  elom  6933  seqomlem2  7406  pssnn  8036  findcard  8057  findcard2  8058  findcard3  8061  fiint  8095  inf0  8374  axinf2  8393  tz9.1  8461  karden  8614  aceq0  8797  dfac5  8807  zfac  9138  brdom3  9204  axpowndlem3  9273  zfcndrep  9288  zfcndac  9293  elgch  9296  engch  9302  axgroth3  9505  axgroth4  9506  elnp  9661  elnpi  9662  infm3  10827  fz1sbc  12236  uzrdgfni  12570  trclfvcotr  13540  relexpindlem  13593  vdwmc2  15463  ramtlecl  15484  ramval  15492  ramub  15497  rami  15499  ramcl  15513  mreexexd  16073  mreexexdOLD  16074  mplsubglem  19197  mpllsslem  19198  istopg  20463  1stccn  21014  iskgen3  21100  fbfinnfr  21393  cnextfun  21616  metcld  22825  metcld2  22826  cusgrauvtxb  25786  chlimi  27277  nmcexi  28071  disjrdx  28588  funcnvmpt  28653  mclsssvlem  30515  mclsval  30516  mclsind  30523  dfon2lem6  30739  dfon2lem7  30740  dfon2lem8  30741  dfon2  30743  sscoid  30992  trer  31282  bj-ssbequ  31620  bj-ssblem1  31621  bj-axext3  31766  bj-axrep1  31785  bj-axrep2  31786  bj-axrep3  31787  bj-axrep4  31788  bj-sbceqgALT  31888  bj-axsep2  31912  bj-nuliota  32009  wl-mo2t  32335  isass  32614  axc11n-16  33040  cdlemefrs29bpre0  34501  elmapintab  36720  cnvcnvintabd  36724  iunrelexpuztr  36829  ntrneiiso  37208  ntrneik2  37209  ntrneix2  37210  ntrneikb  37211  pm14.122b  37445  iotavalb  37452  trsbc  37570  sbcalgOLD  37572  dffo3f  38158  fun2dmnopgexmpl  40152
  Copyright terms: Public domain W3C validator