Theorem albid 2215

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

Syntax hints:   → wi 4   ↔ wb 205  ∀wal 1539  Ⅎwnf 1785

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1913  ax-6 1971  ax-7 2011  ax-12 2171

This theorem depends on definitions:  df-bi 206  df-ex 1782  df-nf 1786

This theorem is referenced by:  nfbidf  2217  dral1vOLD  2367  dral2  2437  dral1  2438  sb4b  2474  sbal1  2527  sbal2  2528  ralbidaOLD  3268  raleqf  3349  intab  4982  fin23lem32  10338  axrepndlem1  10586  axrepndlem2  10587  axrepnd  10588  axunnd  10590  axpowndlem2  10592  axpowndlem4  10594  axregndlem2  10597  axinfndlem1  10599  axinfnd  10600  axacndlem4  10604  axacndlem5  10605  axacnd  10606  iota5f  34688  exrecfnlem  36255  wl-equsald  36403  wl-sbnf1  36415  wl-2sb6d  36418  wl-sbalnae  36422  wl-mo2df  36430  wl-eudf  36432  wl-ax11-lem6  36447  wl-ax11-lem8  36449  ax12eq  37806  ax12el  37807  ax12v2-o  37814  unielss  41957