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  3326  intab  4934  fin23lem32  10258  axrepndlem1  10507  axrepndlem2  10508  axrepnd  10509  axunnd  10511  axpowndlem2  10513  axpowndlem4  10515  axregndlem2  10518  axinfndlem1  10520  axinfnd  10521  axacndlem4  10525  axacndlem5  10526  axacnd  10527  iota5f  35920  mh-setindnd  36669  exrecfnlem  37586  wl-equsald  37746  wl-equsaldv  37747  wl-sbnf1  37762  wl-2sb6d  37765  wl-sbalnae  37769  wl-mo2df  37777  wl-eudf  37779  ax12eq  39269  ax12el  39270  ax12v2-o  39277  unielss  43527  permaxrep  45314  permaxsep  45315