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

Theorem albid 2077
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 2053 . 2 (𝜑 → ∀𝑥𝜑)
3 albid.2 . 2 (𝜑 → (𝜓𝜒))
42, 3albidh 1780 1 (𝜑 → (∀𝑥𝜓 ↔ ∀𝑥𝜒))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 195  wal 1473  wnf 1699
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1713  ax-4 1728  ax-5 1827  ax-6 1875  ax-7 1922  ax-12 2034
This theorem depends on definitions:  df-bi 196  df-ex 1696  df-nf 1701
This theorem is referenced by:  nfbidf  2079  axc15  2291  dral2  2312  dral1  2313  ax12v2OLD  2330  sbal1  2448  sbal2  2449  eubid  2476  ralbida  2965  raleqf  3111  intab  4442  fin23lem32  9049  axrepndlem1  9293  axrepndlem2  9294  axrepnd  9295  axunnd  9297  axpowndlem2  9299  axpowndlem4  9301  axregndlem2  9304  axinfndlem1  9306  axinfnd  9307  axacndlem4  9311  axacndlem5  9312  axacnd  9313  funcnvmptOLD  28850  iota5f  30861  bj-dral1v  31936  wl-equsald  32504  wl-sbnf1  32515  wl-2sb6d  32520  wl-sbalnae  32524  wl-mo2df  32531  wl-eudf  32533  wl-ax11-lem6  32546  wl-ax11-lem8  32548  ax12eq  33244  ax12el  33245  ax12v2-o  33252
  Copyright terms: Public domain W3C validator