Theorem albid 2225

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 2198	. 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 2180

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

This theorem is referenced by:  nfbidf  2227  dral2  2438  dral1  2439  sb4b  2475  sbal1  2528  sbal2  2529  raleqf  3321  intab  4926  fin23lem32  10235  axrepndlem1  10483  axrepndlem2  10484  axrepnd  10485  axunnd  10487  axpowndlem2  10489  axpowndlem4  10491  axregndlem2  10494  axinfndlem1  10496  axinfnd  10497  axacndlem4  10501  axacndlem5  10502  axacnd  10503  iota5f  35768  exrecfnlem  37423  wl-equsald  37583  wl-equsaldv  37584  wl-sbnf1  37599  wl-2sb6d  37602  wl-sbalnae  37606  wl-mo2df  37614  wl-eudf  37616  ax12eq  39039  ax12el  39040  ax12v2-o  39047  unielss  43310  permaxrep  45098  permaxsep  45099