Theorem albid 2215

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

Syntax hints:   → wi 4   ↔ wb 205  ∀wal 1537  Ⅎwnf 1786

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1913  ax-6 1971  ax-7 2011  ax-12 2171

This theorem depends on definitions:  df-bi 206  df-ex 1783  df-nf 1787

This theorem is referenced by:  nfbidf  2217  dral1vOLD  2368  dral2  2438  dral1  2439  sb4b  2475  sb4bOLD  2476  sbal1  2533  sbal2  2534  ralbidaOLD  3160  raleqf  3332  intab  4909  fin23lem32  10100  axrepndlem1  10348  axrepndlem2  10349  axrepnd  10350  axunnd  10352  axpowndlem2  10354  axpowndlem4  10356  axregndlem2  10359  axinfndlem1  10361  axinfnd  10362  axacndlem4  10366  axacndlem5  10367  axacnd  10368  iota5f  33669  exrecfnlem  35550  wl-equsald  35698  wl-sbnf1  35710  wl-2sb6d  35713  wl-sbalnae  35717  wl-mo2df  35725  wl-eudf  35727  wl-ax11-lem6  35741  wl-ax11-lem8  35743  ax12eq  36955  ax12el  36956  ax12v2-o  36963