Theorem albid 2220

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

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

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1792  ax-4 1806  ax-5 1908  ax-6 1965  ax-7 2005  ax-12 2175

This theorem depends on definitions:  df-bi 207  df-ex 1777  df-nf 1781

This theorem is referenced by:  nfbidf  2222  dral1vOLD  2371  dral2  2441  dral1  2442  sb4b  2478  sbal1  2531  sbal2  2532  ralbidaOLD  3269  raleqf  3351  intab  4983  fin23lem32  10382  axrepndlem1  10630  axrepndlem2  10631  axrepnd  10632  axunnd  10634  axpowndlem2  10636  axpowndlem4  10638  axregndlem2  10641  axinfndlem1  10643  axinfnd  10644  axacndlem4  10648  axacndlem5  10649  axacnd  10650  iota5f  35704  exrecfnlem  37362  wl-equsald  37520  wl-equsaldv  37521  wl-sbnf1  37536  wl-2sb6d  37539  wl-sbalnae  37543  wl-mo2df  37551  wl-eudf  37553  wl-ax11-lem6  37571  wl-ax11-lem8  37573  ax12eq  38923  ax12el  38924  ax12v2-o  38931  unielss  43207