Theorem albid 2236

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

Syntax hints:   → wi 4   ↔ wb 208  ∀wal 1546  Ⅎwnf 1791

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1803  ax-4 1817  ax-5 1918  ax-6 1975  ax-7 2016  ax-12 2191

This theorem depends on definitions:  df-bi 209  df-ex 1788  df-nf 1792

This theorem is referenced by:  nfbidf  2238  dral2  2448  dral1  2449  sb4b  2485  sbal1  2538  sbal2  2539  raleqf  3322  intab  4911  fin23lem32  10261  axrepndlem1  10510  axrepndlem2  10511  axrepnd  10512  axunnd  10514  axpowndlem2  10516  axpowndlem4  10518  axregndlem2  10521  axinfndlem1  10523  axinfnd  10524  axacndlem4  10528  axacndlem5  10529  axacnd  10530  iota5f  35967  axtcond  36721  mh-setindnd  36780  bj-axreprepsep  37443  exrecfnlem  37756  wl-equsald  37925  wl-equsaldv  37926  wl-sbnf1  37941  wl-2sb6d  37944  wl-sbalnae  37948  wl-mo2df  37956  wl-eudf  37958  ax12eq  39448  ax12el  39449  ax12v2-o  39456  unielss  43678  permaxrep  45465  permaxsep  45466