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  2442  dral1  2443  sb4b  2479  sbal1  2532  sbal2  2533  raleqf  3318  intab  4920  fin23lem32  10266  axrepndlem1  10515  axrepndlem2  10516  axrepnd  10517  axunnd  10519  axpowndlem2  10521  axpowndlem4  10523  axregndlem2  10526  axinfndlem1  10528  axinfnd  10529  axacndlem4  10533  axacndlem5  10534  axacnd  10535  iota5f  35906  axtcond  36660  mh-setindnd  36719  bj-axreprepsep  37382  exrecfnlem  37695  wl-equsald  37864  wl-equsaldv  37865  wl-sbnf1  37880  wl-2sb6d  37883  wl-sbalnae  37887  wl-mo2df  37895  wl-eudf  37897  ax12eq  39387  ax12el  39388  ax12v2-o  39395  unielss  43646  permaxrep  45433  permaxsep  45434