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

Theorem albid 2255
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 2227 . 2 (𝜑 → ∀𝑥𝜑)
3 albid.2 . 2 (𝜑 → (𝜓𝜒))
42, 3albidh 1963 1 (𝜑 → (∀𝑥𝜓 ↔ ∀𝑥𝜒))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 197  wal 1650  wnf 1878
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1890  ax-4 1904  ax-5 2005  ax-6 2069  ax-7 2105  ax-12 2211
This theorem depends on definitions:  df-bi 198  df-ex 1875  df-nf 1879
This theorem is referenced by:  nfbidf  2257  axc15  2403  dral2  2418  dral1  2419  sbal1  2552  sbal2  2553  mobid  2580  eubidOLD  2617  ralbida  3129  raleqf  3282  intab  4663  fin23lem32  9419  axrepndlem1  9667  axrepndlem2  9668  axrepnd  9669  axunnd  9671  axpowndlem2  9673  axpowndlem4  9675  axregndlem2  9678  axinfndlem1  9680  axinfnd  9681  axacndlem4  9685  axacndlem5  9686  axacnd  9687  iota5f  31984  bj-dral1v  33114  wl-equsald  33682  wl-sbnf1  33694  wl-2sb6d  33698  wl-sbalnae  33702  wl-mo2df  33709  wl-eudf  33711  wl-ax11-lem6  33724  wl-ax11-lem8  33726  ax12eq  34829  ax12el  34830  ax12v2-o  34837
  Copyright terms: Public domain W3C validator