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

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

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