Theorem albid 2258

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

This proof depends on syntax axioms:   → wi 4   ↔ wb 209  ∀wal 1567  Ⅎwnf 1815

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-5 1942  ax-6 1999  ax-7 2040  ax-12 2212

This proof depends on definitions:  df-bi 210  df-ex 1812  df-nf 1816

This theorem is used by:  nfbidf  2260  dral2  2467  dral1  2468  sb4b  2504  sbal1  2557  sbal2  2558  raleqf  3341  intab  4937  fin23lem32  10422  axrepndlem1  10677  axrepndlem2  10678  axrepnd  10679  axunnd  10681  axpowndlem2  10683  axpowndlem4  10685  axregndlem2  10688  axinfndlem1  10690  axinfnd  10691  axacndlem4  10695  axacndlem5  10696  axacnd  10697  iota5f  36489  axtcond  37266  mh-setindnd  37325  bj-axreprepsep  37991  exrecfnlem  38303  wl-equsald  38472  wl-equsaldv  38473  wl-sbnf1  38488  wl-2sb6d  38491  wl-sbalnae  38495  wl-mo2df  38503  wl-eudf  38505  ax12eq  39999  ax12el  40000  ax12v2-o  40007  unielss  44220  permaxrep  45996  permaxsep  45997  alsbid  50898