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

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

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