Theorem albid 2090

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	nf5ri 2065	. 2 |- ( ph -> A. x ph )
3		albid.2	. 2 |- ( ph -> ( ps <-> ch ) )
4	2, 3	albidh 1793	1 |- ( ph -> ( A. x ps <-> A. x ch ) )

Syntax hints:   -> wi 4   <-> wb 196   A.wal 1481   F/wnf 1708

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1722  ax-4 1737  ax-5 1839  ax-6 1888  ax-7 1935  ax-12 2047

This theorem depends on definitions:  df-bi 197  df-ex 1705  df-nf 1710

This theorem is referenced by:  nfbidf  2092  axc15  2303  dral2  2324  dral1  2325  ax12v2OLD  2342  sbal1  2460  sbal2  2461  eubid  2488  ralbida  2982  raleqf  3134  intab  4507  fin23lem32  9166  axrepndlem1  9414  axrepndlem2  9415  axrepnd  9416  axunnd  9418  axpowndlem2  9420  axpowndlem4  9422  axregndlem2  9425  axinfndlem1  9427  axinfnd  9428  axacndlem4  9432  axacndlem5  9433  axacnd  9434  funcnvmptOLD  29467  iota5f  31606  bj-dral1v  32748  wl-equsald  33325  wl-sbnf1  33336  wl-2sb6d  33341  wl-sbalnae  33345  wl-mo2df  33352  wl-eudf  33354  wl-ax11-lem6  33367  wl-ax11-lem8  33369  ax12eq  34226  ax12el  34227  ax12v2-o  34234