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

Theorem albid 2222
 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 1867 1 (𝜑 → (∀𝑥𝜓 ↔ ∀𝑥𝜒))
 Colors of variables: wff setvar class Syntax hints:   → wi 4   ↔ wb 209  ∀wal 1536  Ⅎwnf 1785 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1911  ax-6 1970  ax-7 2015  ax-12 2175 This theorem depends on definitions:  df-bi 210  df-ex 1782  df-nf 1786 This theorem is referenced by:  nfbidf  2224  dral1v  2376  dral2  2449  dral1  2450  sb4b  2488  sb4bOLD  2489  sbal1  2548  sbal2  2549  sbal2OLD  2550  ralbida  3194  raleqf  3350  intab  4869  fin23lem32  9758  axrepndlem1  10006  axrepndlem2  10007  axrepnd  10008  axunnd  10010  axpowndlem2  10012  axpowndlem4  10014  axregndlem2  10017  axinfndlem1  10019  axinfnd  10020  axacndlem4  10024  axacndlem5  10025  axacnd  10026  iota5f  33083  exrecfnlem  34815  wl-equsald  34963  wl-sbnf1  34975  wl-2sb6d  34978  wl-sbalnae  34982  wl-mo2df  34990  wl-eudf  34992  wl-ax11-lem6  35006  wl-ax11-lem8  35008  wl-dfrmof  35039  ax12eq  36256  ax12el  36257  ax12v2-o  36264
 Copyright terms: Public domain W3C validator