Theorem albid 2227

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

Syntax hints:   → wi 4   ↔ wb 206  ∀wal 1539  Ⅎ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 1968  ax-7 2009  ax-12 2182

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

This theorem is referenced by:  nfbidf  2229  dral2  2440  dral1  2441  sb4b  2477  sbal1  2530  sbal2  2531  raleqf  3323  intab  4931  fin23lem32  10252  axrepndlem1  10501  axrepndlem2  10502  axrepnd  10503  axunnd  10505  axpowndlem2  10507  axpowndlem4  10509  axregndlem2  10512  axinfndlem1  10514  axinfnd  10515  axacndlem4  10519  axacndlem5  10520  axacnd  10521  iota5f  35867  exrecfnlem  37523  wl-equsald  37683  wl-equsaldv  37684  wl-sbnf1  37699  wl-2sb6d  37702  wl-sbalnae  37706  wl-mo2df  37714  wl-eudf  37716  ax12eq  39140  ax12el  39141  ax12v2-o  39148  unielss  43402  permaxrep  45189  permaxsep  45190