Theorem albid 2260

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

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

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-12 2215

This proof depends on definitions:  df-bi 210  df-ex 1813  df-nf 1817

This theorem is used by:  nfbidf  2262  dral2  2469  dral1  2470  sb4b  2506  sbal1  2559  sbal2  2560  raleqf  3343  intab  4941  fin23lem32  10349  axrepndlem1  10602  axrepndlem2  10603  axrepnd  10604  axunnd  10606  axpowndlem2  10608  axpowndlem4  10610  axregndlem2  10613  axinfndlem1  10615  axinfnd  10616  axacndlem4  10620  axacndlem5  10621  axacnd  10622  iota5f  36288  axtcond  37082  mh-setindnd  37141  bj-axreprepsep  37805  exrecfnlem  38118  wl-equsald  38287  wl-equsaldv  38288  wl-sbnf1  38303  wl-2sb6d  38306  wl-sbalnae  38310  wl-mo2df  38318  wl-eudf  38320  ax12eq  39799  ax12el  39800  ax12v2-o  39807  unielss  44044  permaxrep  45814  permaxsep  45815  alsbid  50713