Theorem albid 2218

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

Syntax hints:   → wi 4   ↔ wb 205  ∀wal 1539  Ⅎwnf 1789

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1801  ax-4 1815  ax-5 1916  ax-6 1974  ax-7 2014  ax-12 2174

This theorem depends on definitions:  df-bi 206  df-ex 1786  df-nf 1790

This theorem is referenced by:  nfbidf  2220  dral1vOLD  2369  dral2  2439  dral1  2440  sb4b  2476  sb4bOLD  2477  sbal1  2534  sbal2  2535  ralbidaOLD  3159  raleqf  3330  intab  4914  fin23lem32  10084  axrepndlem1  10332  axrepndlem2  10333  axrepnd  10334  axunnd  10336  axpowndlem2  10338  axpowndlem4  10340  axregndlem2  10343  axinfndlem1  10345  axinfnd  10346  axacndlem4  10350  axacndlem5  10351  axacnd  10352  iota5f  33648  exrecfnlem  35529  wl-equsald  35677  wl-sbnf1  35689  wl-2sb6d  35692  wl-sbalnae  35696  wl-mo2df  35704  wl-eudf  35706  wl-ax11-lem6  35720  wl-ax11-lem8  35722  ax12eq  36934  ax12el  36935  ax12v2-o  36942