Theorem albid 2128

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	nf5ri 2103	. 2 ⊢ (𝜑 → ∀𝑥𝜑)
3		albid.2	. 2 ⊢ (𝜑 → (𝜓 ↔ 𝜒))
4	2, 3	albidh 1833	1 ⊢ (𝜑 → (∀𝑥𝜓 ↔ ∀𝑥𝜒))

Syntax hints:   → wi 4   ↔ wb 196  ∀wal 1521  Ⅎwnf 1748

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1762  ax-4 1777  ax-5 1879  ax-6 1945  ax-7 1981  ax-12 2087

This theorem depends on definitions:  df-bi 197  df-ex 1745  df-nf 1750

This theorem is referenced by:  nfbidf  2130  axc15  2339  dral2  2355  dral1  2356  sbal1  2488  sbal2  2489  eubid  2516  ralbida  3011  raleqf  3164  intab  4539  fin23lem32  9204  axrepndlem1  9452  axrepndlem2  9453  axrepnd  9454  axunnd  9456  axpowndlem2  9458  axpowndlem4  9460  axregndlem2  9463  axinfndlem1  9465  axinfnd  9466  axacndlem4  9470  axacndlem5  9471  axacnd  9472  funcnvmptOLD  29595  iota5f  31732  bj-dral1v  32873  wl-equsald  33455  wl-sbnf1  33466  wl-2sb6d  33471  wl-sbalnae  33475  wl-mo2df  33482  wl-eudf  33484  wl-ax11-lem6  33497  wl-ax11-lem8  33499  ax12eq  34545  ax12el  34546  ax12v2-o  34553