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

Theorem albid 2220
Description: Formula-building rule for universal quantifier (deduction form). (Contributed by Mario Carneiro, 24-Sep-2016.)
Hypotheses
Ref Expression
albid.1 𝑥𝜑
albid.2 (𝜑 → (𝜓𝜒))
Assertion
Ref Expression
albid (𝜑 → (∀𝑥𝜓 ↔ ∀𝑥𝜒))

Proof of Theorem albid
StepHypRef Expression
1 albid.1 . . 3 𝑥𝜑
21nf5ri 2193 . 2 (𝜑 → ∀𝑥𝜑)
3 albid.2 . 2 (𝜑 → (𝜓𝜒))
42, 3albidh 1874 1 (𝜑 → (∀𝑥𝜓 ↔ ∀𝑥𝜒))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 209  wal 1541  wnf 1791
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1803  ax-4 1817  ax-5 1918  ax-6 1976  ax-7 2016  ax-12 2175
This theorem depends on definitions:  df-bi 210  df-ex 1788  df-nf 1792
This theorem is referenced by:  nfbidf  2222  dral1v  2368  dral2  2437  dral1  2438  sb4b  2474  sb4bOLD  2475  sbal1  2532  sbal2  2533  ralbida  3153  raleqf  3309  intab  4889  fin23lem32  9958  axrepndlem1  10206  axrepndlem2  10207  axrepnd  10208  axunnd  10210  axpowndlem2  10212  axpowndlem4  10214  axregndlem2  10217  axinfndlem1  10219  axinfnd  10220  axacndlem4  10224  axacndlem5  10225  axacnd  10226  iota5f  33384  exrecfnlem  35287  wl-equsald  35435  wl-sbnf1  35447  wl-2sb6d  35450  wl-sbalnae  35454  wl-mo2df  35462  wl-eudf  35464  wl-ax11-lem6  35478  wl-ax11-lem8  35480  ax12eq  36692  ax12el  36693  ax12v2-o  36700
  Copyright terms: Public domain W3C validator