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

Theorem albid 2088
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 2063 . 2 (𝜑 → ∀𝑥𝜑)
3 albid.2 . 2 (𝜑 → (𝜓𝜒))
42, 3albidh 1790 1 (𝜑 → (∀𝑥𝜓 ↔ ∀𝑥𝜒))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 196  wal 1478  wnf 1705
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1719  ax-4 1734  ax-5 1836  ax-6 1885  ax-7 1932  ax-12 2044
This theorem depends on definitions:  df-bi 197  df-ex 1702  df-nf 1707
This theorem is referenced by:  nfbidf  2090  axc15  2302  dral2  2323  dral1  2324  ax12v2OLD  2341  sbal1  2459  sbal2  2460  eubid  2487  ralbida  2977  raleqf  3126  intab  4477  fin23lem32  9118  axrepndlem1  9366  axrepndlem2  9367  axrepnd  9368  axunnd  9370  axpowndlem2  9372  axpowndlem4  9374  axregndlem2  9377  axinfndlem1  9379  axinfnd  9380  axacndlem4  9384  axacndlem5  9385  axacnd  9386  funcnvmptOLD  29333  iota5f  31350  bj-dral1v  32426  wl-equsald  32992  wl-sbnf1  33003  wl-2sb6d  33008  wl-sbalnae  33012  wl-mo2df  33019  wl-eudf  33021  wl-ax11-lem6  33034  wl-ax11-lem8  33036  ax12eq  33741  ax12el  33742  ax12v2-o  33749
  Copyright terms: Public domain W3C validator