Theorem albid 2216

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

Syntax hints:   → wi 4   ↔ wb 205  ∀wal 1540  Ⅎwnf 1786

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-12 2172

This theorem depends on definitions:  df-bi 206  df-ex 1783  df-nf 1787

This theorem is referenced by:  nfbidf  2218  dral1vOLD  2368  dral2  2438  dral1  2439  sb4b  2475  sbal1  2528  sbal2  2529  ralbidaOLD  3269  raleqf  3350  intab  4983  fin23lem32  10339  axrepndlem1  10587  axrepndlem2  10588  axrepnd  10589  axunnd  10591  axpowndlem2  10593  axpowndlem4  10595  axregndlem2  10598  axinfndlem1  10600  axinfnd  10601  axacndlem4  10605  axacndlem5  10606  axacnd  10607  iota5f  34693  exrecfnlem  36260  wl-equsald  36408  wl-sbnf1  36420  wl-2sb6d  36423  wl-sbalnae  36427  wl-mo2df  36435  wl-eudf  36437  wl-ax11-lem6  36452  wl-ax11-lem8  36454  ax12eq  37811  ax12el  37812  ax12v2-o  37819  unielss  41967