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

Theorem albid 1821
Description: Formula-building rule for universal quantifier (deduction rule). (Contributed by Mario Carneiro, 24-Sep-2016.)
Hypotheses
Ref Expression
albid.1  |-  F/ x ph
albid.2  |-  ( ph  ->  ( ps  <->  ch )
)
Assertion
Ref Expression
albid  |-  ( ph  ->  ( A. x ps  <->  A. x ch ) )

Proof of Theorem albid
StepHypRef Expression
1 albid.1 . . 3  |-  F/ x ph
21nfri 1810 . 2  |-  ( ph  ->  A. x ph )
3 albid.2 . 2  |-  ( ph  ->  ( ps  <->  ch )
)
42, 3albidh 1643 1  |-  ( ph  ->  ( A. x ps  <->  A. x ch ) )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    <-> wb 184   A.wal 1368   F/wnf 1590
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1592  ax-4 1603  ax-5 1671  ax-6 1710  ax-7 1730  ax-12 1794
This theorem depends on definitions:  df-bi 185  df-ex 1588  df-nf 1591
This theorem is referenced by:  nfbidf  1823  dral2  2023  dral1  2024  ax12v2  2040  sbal1  2178  sbal2  2180  sbal2OLD  2191  ax12eq  2249  ax12el  2250  ax12v2-o  2257  eubid  2281  ralbidaOLD  2834  raleqf  3011  intab  4258  fin23lem32  8616  axrepndlem1  8859  axrepndlem2  8860  axrepnd  8861  axunnd  8863  axpowndlem2  8865  axpowndlem2OLD  8866  axpowndlem4  8869  axregndlem2  8872  axinfndlem1  8875  axinfnd  8876  axacndlem4  8880  axacndlem5  8881  axacnd  8882  funcnvmptOLD  26122  iota5f  27517  wl-equsald  28508  wl-sbnf1  28519  wl-2sb6d  28524  wl-sbalnae  28528  wl-mo2dnae  28535  wl-ax11-lem6  28546  wl-ax11-lem8  28548  bj-dral1v  32563  bj-axc15v  32567
  Copyright terms: Public domain W3C validator