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

Theorem albid 1909
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 1898 . 2  |-  ( ph  ->  A. x ph )
3 albid.2 . 2  |-  ( ph  ->  ( ps  <->  ch )
)
42, 3albidh 1696 1  |-  ( ph  ->  ( A. x ps  <->  A. x ch ) )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    <-> wb 184   A.wal 1403   F/wnf 1637
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1639  ax-4 1652  ax-5 1725  ax-6 1771  ax-7 1814  ax-12 1878
This theorem depends on definitions:  df-bi 185  df-ex 1634  df-nf 1638
This theorem is referenced by:  nfbidf  1911  dral2  2092  dral1  2093  ax12v2  2109  sbal1  2228  sbal2  2229  eubid  2258  ralbida  2836  raleqf  2999  intab  4257  fin23lem32  8755  axrepndlem1  8998  axrepndlem2  8999  axrepnd  9000  axunnd  9002  axpowndlem2  9004  axpowndlem4  9006  axregndlem2  9009  axinfndlem1  9012  axinfnd  9013  axacndlem4  9017  axacndlem5  9018  axacnd  9019  funcnvmptOLD  27938  iota5f  29918  bj-dral1v  30877  bj-axc15v  30881  wl-equsald  31344  wl-sbnf1  31355  wl-2sb6d  31360  wl-sbalnae  31364  wl-mo2dnae  31371  wl-ax11-lem6  31382  wl-ax11-lem8  31384  ax12eq  31944  ax12el  31945  ax12v2-o  31952
  Copyright terms: Public domain W3C validator