Theorem albid 2264

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

Syntax hints:   → wi 4   ↔ wb 209  ∀wal 1565  Ⅎwnf 1810

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1822  ax-4 1836  ax-5 1937  ax-6 1994  ax-7 2035  ax-12 2219

This theorem depends on definitions:  df-bi 210  df-ex 1807  df-nf 1811

This theorem is referenced by:  nfbidf  2266  dral2  2476  dral1  2477  sb4b  2513  sbal1  2566  sbal2  2567  raleqf  3352  intab  4947  fin23lem32  10330  axrepndlem1  10579  axrepndlem2  10580  axrepnd  10581  axunnd  10583  axpowndlem2  10585  axpowndlem4  10587  axregndlem2  10590  axinfndlem1  10592  axinfnd  10593  axacndlem4  10597  axacndlem5  10598  axacnd  10599  iota5f  36151  axtcond  36914  mh-setindnd  36973  bj-axreprepsep  37637  exrecfnlem  37950  wl-equsald  38119  wl-equsaldv  38120  wl-sbnf1  38135  wl-2sb6d  38138  wl-sbalnae  38142  wl-mo2df  38150  wl-eudf  38152  ax12eq  39642  ax12el  39643  ax12v2-o  39650  unielss  43874  permaxrep  45644  permaxsep  45645  alsbid  50502