Theorem albid 1885

Description: Formula-building rule for universal quantifier (deduction rule). (Contributed by Mario Carneiro, 24-Sep-2016.)

Hypotheses

Ref	Expression
albid.1
albid.2

Assertion

Ref	Expression
albid

Proof of Theorem albid

Step	Hyp	Ref	Expression
1		albid.1	. . 3
2	1	nfri 1874	. 2
3		albid.2	. 2
4	2, 3	albidh 1675	1

Syntax hints:  ->wi 4  <->wb 184  A.wal 1393  F/wnf 1616

This theorem is referenced by:  nfbidf  1887  dral2  2066  dral1  2067  ax12v2  2083  sbal1  2204  sbal2  2205  ax12eq  2271  ax12el  2272  ax12v2-o  2279  eubid  2302  ralbida  2890  raleqf  3050  intab  4317  fin23lem32  8745  axrepndlem1  8988  axrepndlem2  8989  axrepnd  8990  axunnd  8992  axpowndlem2  8994  axpowndlem2OLD  8995  axpowndlem4  8998  axregndlem2  9001  axinfndlem1  9004  axinfnd  9005  axacndlem4  9009  axacndlem5  9010  axacnd  9011  funcnvmptOLD  27509  iota5f  29102  wl-equsald  29992  wl-sbnf1  30003  wl-2sb6d  30008  wl-sbalnae  30012  wl-mo2dnae  30019  wl-ax11-lem6  30030  wl-ax11-lem8  30032  bj-dral1v  34326  bj-axc15v  34330

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1618  ax-4 1631  ax-5 1704  ax-6 1747  ax-7 1790  ax-12 1854

This theorem depends on definitions:  df-bi 185  df-ex 1613  df-nf 1617