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 1870	1 ⊢ (𝜑 → (∀𝑥𝜓 ↔ ∀𝑥𝜒))

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

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1799  ax-4 1813  ax-5 1914  ax-6 1972  ax-7 2012  ax-12 2173

This theorem depends on definitions:  df-bi 206  df-ex 1784  df-nf 1788

This theorem is referenced by:  nfbidf  2220  dral1vOLD  2368  dral2  2438  dral1  2439  sb4b  2475  sb4bOLD  2476  sbal1  2533  sbal2  2534  ralbidaOLD  3157  raleqf  3323  intab  4906  fin23lem32  10031  axrepndlem1  10279  axrepndlem2  10280  axrepnd  10281  axunnd  10283  axpowndlem2  10285  axpowndlem4  10287  axregndlem2  10290  axinfndlem1  10292  axinfnd  10293  axacndlem4  10297  axacndlem5  10298  axacnd  10299  iota5f  33571  exrecfnlem  35477  wl-equsald  35625  wl-sbnf1  35637  wl-2sb6d  35640  wl-sbalnae  35644  wl-mo2df  35652  wl-eudf  35654  wl-ax11-lem6  35668  wl-ax11-lem8  35670  ax12eq  36882  ax12el  36883  ax12v2-o  36890