Theorem albid 2222

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 1866	1 ⊢ (𝜑 → (∀𝑥𝜓 ↔ ∀𝑥𝜒))

Syntax hints:   → wi 4   ↔ wb 206  ∀wal 1538  Ⅎwnf 1783

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2007  ax-12 2177

This theorem depends on definitions:  df-bi 207  df-ex 1780  df-nf 1784

This theorem is referenced by:  nfbidf  2224  dral1vOLD  2373  dral2  2443  dral1  2444  sb4b  2480  sbal1  2533  sbal2  2534  ralbidaOLD  3271  raleqf  3353  intab  4978  fin23lem32  10384  axrepndlem1  10632  axrepndlem2  10633  axrepnd  10634  axunnd  10636  axpowndlem2  10638  axpowndlem4  10640  axregndlem2  10643  axinfndlem1  10645  axinfnd  10646  axacndlem4  10650  axacndlem5  10651  axacnd  10652  iota5f  35724  exrecfnlem  37380  wl-equsald  37540  wl-equsaldv  37541  wl-sbnf1  37556  wl-2sb6d  37559  wl-sbalnae  37563  wl-mo2df  37571  wl-eudf  37573  wl-ax11-lem6  37591  wl-ax11-lem8  37593  ax12eq  38942  ax12el  38943  ax12v2-o  38950  unielss  43230