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

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

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