Theorem albid 2220

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

Syntax hints:   → wi 4   ↔ wb 209  ∀wal 1541  Ⅎwnf 1791

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1803  ax-4 1817  ax-5 1918  ax-6 1976  ax-7 2016  ax-12 2175

This theorem depends on definitions:  df-bi 210  df-ex 1788  df-nf 1792

This theorem is referenced by:  nfbidf  2222  dral1v  2368  dral2  2437  dral1  2438  sb4b  2474  sb4bOLD  2475  sbal1  2532  sbal2  2533  ralbida  3153  raleqf  3309  intab  4889  fin23lem32  9958  axrepndlem1  10206  axrepndlem2  10207  axrepnd  10208  axunnd  10210  axpowndlem2  10212  axpowndlem4  10214  axregndlem2  10217  axinfndlem1  10219  axinfnd  10220  axacndlem4  10224  axacndlem5  10225  axacnd  10226  iota5f  33384  exrecfnlem  35287  wl-equsald  35435  wl-sbnf1  35447  wl-2sb6d  35450  wl-sbalnae  35454  wl-mo2df  35462  wl-eudf  35464  wl-ax11-lem6  35478  wl-ax11-lem8  35480  ax12eq  36692  ax12el  36693  ax12v2-o  36700