Theorem albid 2223

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

Syntax hints:   → wi 4   ↔ wb 206  ∀wal 1535  Ⅎwnf 1781

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1793  ax-4 1807  ax-5 1909  ax-6 1967  ax-7 2007  ax-12 2178

This theorem depends on definitions:  df-bi 207  df-ex 1778  df-nf 1782

This theorem is referenced by:  nfbidf  2225  dral1vOLD  2376  dral2  2446  dral1  2447  sb4b  2483  sbal1  2536  sbal2  2537  ralbidaOLD  3277  raleqf  3361  intab  5002  fin23lem32  10413  axrepndlem1  10661  axrepndlem2  10662  axrepnd  10663  axunnd  10665  axpowndlem2  10667  axpowndlem4  10669  axregndlem2  10672  axinfndlem1  10674  axinfnd  10675  axacndlem4  10679  axacndlem5  10680  axacnd  10681  iota5f  35686  exrecfnlem  37345  wl-equsald  37493  wl-equsaldv  37494  wl-sbnf1  37509  wl-2sb6d  37512  wl-sbalnae  37516  wl-mo2df  37524  wl-eudf  37526  wl-ax11-lem6  37544  wl-ax11-lem8  37546  ax12eq  38897  ax12el  38898  ax12v2-o  38905  unielss  43179