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

Theorem albid 1828
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 1817 . 2  |-  ( ph  ->  A. x ph )
3 albid.2 . 2  |-  ( ph  ->  ( ps  <->  ch )
)
42, 3albidh 1647 1  |-  ( ph  ->  ( A. x ps  <->  A. x ch ) )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    <-> wb 184   A.wal 1372   F/wnf 1594
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1596  ax-4 1607  ax-5 1675  ax-6 1714  ax-7 1734  ax-12 1798
This theorem depends on definitions:  df-bi 185  df-ex 1592  df-nf 1595
This theorem is referenced by:  nfbidf  1830  dral2  2034  dral1  2035  ax12v2  2051  sbal1  2188  sbal2  2190  sbal2OLD  2201  ax12eq  2259  ax12el  2260  ax12v2-o  2267  eubid  2291  ralbida  2892  raleqf  3049  intab  4307  fin23lem32  8715  axrepndlem1  8958  axrepndlem2  8959  axrepnd  8960  axunnd  8962  axpowndlem2  8964  axpowndlem2OLD  8965  axpowndlem4  8968  axregndlem2  8971  axinfndlem1  8974  axinfnd  8975  axacndlem4  8979  axacndlem5  8980  axacnd  8981  funcnvmptOLD  27169  iota5f  28565  wl-equsald  29557  wl-sbnf1  29568  wl-2sb6d  29573  wl-sbalnae  29577  wl-mo2dnae  29584  wl-ax11-lem6  29595  wl-ax11-lem8  29597  bj-dral1v  33284  bj-axc15v  33288
  Copyright terms: Public domain W3C validator