Theorem albid 2230

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

Syntax hints:   → wi 4   ↔ wb 206  ∀wal 1540  Ⅎ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 1912  ax-6 1969  ax-7 2010  ax-12 2185

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

This theorem is referenced by:  nfbidf  2232  dral2  2443  dral1  2444  sb4b  2480  sbal1  2533  sbal2  2534  raleqf  3327  intab  4935  fin23lem32  10268  axrepndlem1  10517  axrepndlem2  10518  axrepnd  10519  axunnd  10521  axpowndlem2  10523  axpowndlem4  10525  axregndlem2  10528  axinfndlem1  10530  axinfnd  10531  axacndlem4  10535  axacndlem5  10536  axacnd  10537  iota5f  35946  mh-setindnd  36695  bj-axreprepsep  37350  exrecfnlem  37661  wl-equsald  37823  wl-equsaldv  37824  wl-sbnf1  37839  wl-2sb6d  37842  wl-sbalnae  37846  wl-mo2df  37854  wl-eudf  37856  ax12eq  39346  ax12el  39347  ax12v2-o  39354  unielss  43604  permaxrep  45391  permaxsep  45392