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

Syntax hints:   → wi 4   ↔ wb 206  ∀wal 1538  Ⅎwnf 1783

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-12 2178

This theorem depends on definitions:  df-bi 207  df-ex 1780  df-nf 1784

This theorem is referenced by:  nfbidf  2225  dral2  2437  dral1  2438  sb4b  2474  sbal1  2527  sbal2  2528  raleqf  3331  intab  4945  fin23lem32  10304  axrepndlem1  10552  axrepndlem2  10553  axrepnd  10554  axunnd  10556  axpowndlem2  10558  axpowndlem4  10560  axregndlem2  10563  axinfndlem1  10565  axinfnd  10566  axacndlem4  10570  axacndlem5  10571  axacnd  10572  iota5f  35718  exrecfnlem  37374  wl-equsald  37534  wl-equsaldv  37535  wl-sbnf1  37550  wl-2sb6d  37553  wl-sbalnae  37557  wl-mo2df  37565  wl-eudf  37567  wl-ax11-lem6  37585  wl-ax11-lem8  37587  ax12eq  38941  ax12el  38942  ax12v2-o  38949  unielss  43214  permaxrep  45003  permaxsep  45004