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  2372  dral2  2442  dral1  2443  sb4b  2479  sbal1  2532  sbal2  2533  raleqf  3332  intab  4954  fin23lem32  10358  axrepndlem1  10606  axrepndlem2  10607  axrepnd  10608  axunnd  10610  axpowndlem2  10612  axpowndlem4  10614  axregndlem2  10617  axinfndlem1  10619  axinfnd  10620  axacndlem4  10624  axacndlem5  10625  axacnd  10626  iota5f  35741  exrecfnlem  37397  wl-equsald  37557  wl-equsaldv  37558  wl-sbnf1  37573  wl-2sb6d  37576  wl-sbalnae  37580  wl-mo2df  37588  wl-eudf  37590  wl-ax11-lem6  37608  wl-ax11-lem8  37610  ax12eq  38959  ax12el  38960  ax12v2-o  38967  unielss  43242  permaxrep  45031  permaxsep  45032