Theorem albid 2262

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 2235	. 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 1945  ax-6 2002  ax-7 2043  ax-12 2216

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

This theorem is used by:  nfbidf  2264  dral2  2470  dral1  2471  sb4b  2507  sbal1  2560  sbal2  2561  raleqf  3345  intab  4941  fin23lem32  10446  axrepndlem1  10701  axrepndlem2  10702  axrepnd  10703  axunnd  10705  axpowndlem2  10707  axpowndlem4  10709  axregndlem2  10712  axinfndlem1  10714  axinfnd  10715  axacndlem4  10719  axacndlem5  10720  axacnd  10721  srepdflem2  36085  iota5f  36666  axtcond  37443  mh-setindnd  37502  bj-axreprepsep  38181  exrecfnlem  38493  wl-equsald  38662  wl-equsaldv  38663  wl-sbnf1  38678  wl-2sb6d  38681  wl-sbalnae  38685  wl-mo2df  38693  wl-eudf  38695  ax12eq  40189  ax12el  40190  ax12v2-o  40197  unielss  44410  permaxrep  46189  permaxsep  46190  alsbid  51176