Theorem albid 2224

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

Syntax hints:   → wi 4   ↔ wb 208  ∀wal 1535  Ⅎwnf 1784

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1970  ax-7 2015  ax-12 2177

This theorem depends on definitions:  df-bi 209  df-ex 1781  df-nf 1785

This theorem is referenced by:  nfbidf  2226  dral1v  2387  dral2  2460  dral1  2461  sb4b  2499  sb4bOLD  2500  sbal1  2572  sbal2  2573  sbal2OLD  2574  ralbida  3232  raleqf  3399  intab  4908  fin23lem32  9768  axrepndlem1  10016  axrepndlem2  10017  axrepnd  10018  axunnd  10020  axpowndlem2  10022  axpowndlem4  10024  axregndlem2  10027  axinfndlem1  10029  axinfnd  10030  axacndlem4  10034  axacndlem5  10035  axacnd  10036  iota5f  32957  exrecfnlem  34662  wl-equsald  34781  wl-sbnf1  34793  wl-2sb6d  34796  wl-sbalnae  34800  wl-mo2df  34808  wl-eudf  34810  wl-ax11-lem6  34824  wl-ax11-lem8  34826  wl-dfrmof  34857  ax12eq  36079  ax12el  36080  ax12v2-o  36087