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

Theorem albid 1983
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 1972 . 2  |-  ( ph  ->  A. x ph )
3 albid.2 . 2  |-  ( ph  ->  ( ps  <->  ch )
)
42, 3albidh 1734 1  |-  ( ph  ->  ( A. x ps  <->  A. x ch ) )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    <-> wb 189   A.wal 1450   F/wnf 1675
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1677  ax-4 1690  ax-5 1766  ax-6 1813  ax-7 1859  ax-12 1950
This theorem depends on definitions:  df-bi 190  df-ex 1672  df-nf 1676
This theorem is referenced by:  nfbidf  1985  axc15  2153  dral2  2173  dral1  2174  ax12v2OLD  2191  sbal1  2309  sbal2  2310  eubid  2337  ralbida  2825  raleqf  2969  intab  4256  fin23lem32  8792  axrepndlem1  9035  axrepndlem2  9036  axrepnd  9037  axunnd  9039  axpowndlem2  9041  axpowndlem4  9043  axregndlem2  9046  axinfndlem1  9048  axinfnd  9049  axacndlem4  9053  axacndlem5  9054  axacnd  9055  funcnvmptOLD  28345  iota5f  30429  bj-dral1v  31424  bj-axc15v  31428  wl-equsald  31942  wl-sbnf1  31953  wl-2sb6d  31958  wl-sbalnae  31962  wl-mo2df  31969  wl-eudf  31971  wl-ax11-lem6  31984  wl-ax11-lem8  31986  ax12eq  32576  ax12el  32577  ax12v2-o  32584
  Copyright terms: Public domain W3C validator