Theorem albid 2259

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

Syntax hints:   → wi 4   ↔ wb 208  ∀wal 1560  Ⅎwnf 1805

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1817  ax-4 1831  ax-5 1932  ax-6 1989  ax-7 2030  ax-12 2214

This theorem depends on definitions:  df-bi 209  df-ex 1802  df-nf 1806

This theorem is referenced by:  nfbidf  2261  dral2  2471  dral1  2472  sb4b  2508  sbal1  2561  sbal2  2562  raleqf  3345  intab  4938  fin23lem32  10303  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  36079  axtcond  36843  mh-setindnd  36902  bj-axreprepsep  37565  exrecfnlem  37878  wl-equsald  38047  wl-equsaldv  38048  wl-sbnf1  38063  wl-2sb6d  38066  wl-sbalnae  38070  wl-mo2df  38078  wl-eudf  38080  ax12eq  39570  ax12el  39571  ax12v2-o  39578  unielss  43800  permaxrep  45587  permaxsep  45588