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

Theorem albid 2128
 Description: Formula-building rule for universal quantifier (deduction rule). (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 2103 . 2 (𝜑 → ∀𝑥𝜑)
3 albid.2 . 2 (𝜑 → (𝜓𝜒))
42, 3albidh 1833 1 (𝜑 → (∀𝑥𝜓 ↔ ∀𝑥𝜒))
 Colors of variables: wff setvar class Syntax hints:   → wi 4   ↔ wb 196  ∀wal 1521  Ⅎwnf 1748 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1762  ax-4 1777  ax-5 1879  ax-6 1945  ax-7 1981  ax-12 2087 This theorem depends on definitions:  df-bi 197  df-ex 1745  df-nf 1750 This theorem is referenced by:  nfbidf  2130  axc15  2339  dral2  2355  dral1  2356  sbal1  2488  sbal2  2489  eubid  2516  ralbida  3011  raleqf  3164  intab  4539  fin23lem32  9204  axrepndlem1  9452  axrepndlem2  9453  axrepnd  9454  axunnd  9456  axpowndlem2  9458  axpowndlem4  9460  axregndlem2  9463  axinfndlem1  9465  axinfnd  9466  axacndlem4  9470  axacndlem5  9471  axacnd  9472  funcnvmptOLD  29595  iota5f  31732  bj-dral1v  32873  wl-equsald  33455  wl-sbnf1  33466  wl-2sb6d  33471  wl-sbalnae  33475  wl-mo2df  33482  wl-eudf  33484  wl-ax11-lem6  33497  wl-ax11-lem8  33499  ax12eq  34545  ax12el  34546  ax12v2-o  34553
 Copyright terms: Public domain W3C validator