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  3319  intab  4921  fin23lem32  10261  axrepndlem1  10510  axrepndlem2  10511  axrepnd  10512  axunnd  10514  axpowndlem2  10516  axpowndlem4  10518  axregndlem2  10521  axinfndlem1  10523  axinfnd  10524  axacndlem4  10528  axacndlem5  10529  axacnd  10530  iota5f  35926  axtcond  36680  mh-setindnd  36739  bj-axreprepsep  37402  exrecfnlem  37713  wl-equsald  37882  wl-equsaldv  37883  wl-sbnf1  37898  wl-2sb6d  37901  wl-sbalnae  37905  wl-mo2df  37913  wl-eudf  37915  ax12eq  39405  ax12el  39406  ax12v2-o  39413  unielss  43668  permaxrep  45455  permaxsep  45456