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

Step	Hyp	Ref	Expression
1		albid.1	. . 3 |- F/ x ph
2	1	nfri 1817	. 2 |- ( ph -> A. x ph )
3		albid.2	. 2 |- ( ph -> ( ps <-> ch ) )
4	2, 3	albidh 1647	1 |- ( ph -> ( A. x ps <-> A. x ch ) )

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