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

Theorem albid 1935
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 1924 . 2  |-  ( ph  ->  A. x ph )
3 albid.2 . 2  |-  ( ph  ->  ( ps  <->  ch )
)
42, 3albidh 1720 1  |-  ( ph  ->  ( A. x ps  <->  A. x ch ) )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    <-> wb 187   A.wal 1435   F/wnf 1663
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1665  ax-4 1678  ax-5 1748  ax-6 1794  ax-7 1838  ax-12 1904
This theorem depends on definitions:  df-bi 188  df-ex 1660  df-nf 1664
This theorem is referenced by:  nfbidf  1937  dral2  2119  dral1  2120  ax12v2  2136  sbal1  2253  sbal2  2254  eubid  2282  ralbida  2856  raleqf  3019  intab  4280  fin23lem32  8770  axrepndlem1  9013  axrepndlem2  9014  axrepnd  9015  axunnd  9017  axpowndlem2  9019  axpowndlem4  9021  axregndlem2  9024  axinfndlem1  9026  axinfnd  9027  axacndlem4  9031  axacndlem5  9032  axacnd  9033  funcnvmptOLD  28251  iota5f  30346  bj-dral1v  31307  bj-axc15v  31311  wl-equsald  31780  wl-sbnf1  31791  wl-2sb6d  31796  wl-sbalnae  31800  wl-mo2df  31807  wl-eudf  31809  wl-ax12v3  31820  wl-ax11-lem6  31828  wl-ax11-lem8  31830  ax12eq  32425  ax12el  32426  ax12v2-o  32433
  Copyright terms: Public domain W3C validator