Theorem albid 2258

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

This proof depends on syntax axioms:   → wi 4   ↔ wb 209  ∀wal 1568  Ⅎwnf 1813

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1825  ax-4 1839  ax-5 1940  ax-6 1997  ax-7 2038  ax-12 2213

This proof depends on definitions:  df-bi 210  df-ex 1810  df-nf 1814

This theorem is used by:  nfbidf  2260  dral2  2470  dral1  2471  sb4b  2507  sbal1  2560  sbal2  2561  raleqf  3345  intab  4943  fin23lem32  10332  axrepndlem1  10581  axrepndlem2  10582  axrepnd  10583  axunnd  10585  axpowndlem2  10587  axpowndlem4  10589  axregndlem2  10592  axinfndlem1  10594  axinfnd  10595  axacndlem4  10599  axacndlem5  10600  axacnd  10601  iota5f  36224  axtcond  37017  mh-setindnd  37076  bj-axreprepsep  37740  exrecfnlem  38053  wl-equsald  38222  wl-equsaldv  38223  wl-sbnf1  38238  wl-2sb6d  38241  wl-sbalnae  38245  wl-mo2df  38253  wl-eudf  38255  ax12eq  39743  ax12el  39744  ax12v2-o  39751  unielss  43973  permaxrep  45743  permaxsep  45744  alsbid  50608