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  2436  dral1  2437  sb4b  2473  sbal1  2526  sbal2  2527  raleqf  3329  intab  4942  fin23lem32  10297  axrepndlem1  10545  axrepndlem2  10546  axrepnd  10547  axunnd  10549  axpowndlem2  10551  axpowndlem4  10553  axregndlem2  10556  axinfndlem1  10558  axinfnd  10559  axacndlem4  10563  axacndlem5  10564  axacnd  10565  iota5f  35711  exrecfnlem  37367  wl-equsald  37527  wl-equsaldv  37528  wl-sbnf1  37543  wl-2sb6d  37546  wl-sbalnae  37550  wl-mo2df  37558  wl-eudf  37560  wl-ax11-lem6  37578  wl-ax11-lem8  37580  ax12eq  38934  ax12el  38935  ax12v2-o  38942  unielss  43207  permaxrep  44996  permaxsep  44997