Theorem albid 2224

Description: Formula-building rule for universal quantifier (deduction form). (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 2195	. 2 ⊢ (𝜑 → ∀𝑥𝜑)
3		albid.2	. 2 ⊢ (𝜑 → (𝜓 ↔ 𝜒))
4	2, 3	albidh 1867	1 ⊢ (𝜑 → (∀𝑥𝜓 ↔ ∀𝑥𝜒))

Syntax hints:   → wi 4   ↔ wb 208  ∀wal 1535  Ⅎwnf 1784

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1970  ax-7 2015  ax-12 2177

This theorem depends on definitions:  df-bi 209  df-ex 1781  df-nf 1785

This theorem is referenced by:  nfbidf  2226  dral1v  2387  dral2  2460  dral1  2461  sb4b  2499  sb4bOLD  2500  sbal1  2572  sbal2  2573  sbal2OLD  2574  ralbida  3230  raleqf  3397  intab  4906  fin23lem32  9766  axrepndlem1  10014  axrepndlem2  10015  axrepnd  10016  axunnd  10018  axpowndlem2  10020  axpowndlem4  10022  axregndlem2  10025  axinfndlem1  10027  axinfnd  10028  axacndlem4  10032  axacndlem5  10033  axacnd  10034  iota5f  32955  exrecfnlem  34663  wl-equsald  34794  wl-sbnf1  34806  wl-2sb6d  34809  wl-sbalnae  34813  wl-mo2df  34821  wl-eudf  34823  wl-ax11-lem6  34837  wl-ax11-lem8  34839  wl-dfrmof  34870  ax12eq  36092  ax12el  36093  ax12v2-o  36100