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 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 2213

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

This theorem is used by:  nfbidf  2260  dral2  2467  dral1  2468  sb4b  2504  sbal1  2557  sbal2  2558  raleqf  3341  intab  4938  fin23lem32  10371  axrepndlem1  10626  axrepndlem2  10627  axrepnd  10628  axunnd  10630  axpowndlem2  10632  axpowndlem4  10634  axregndlem2  10637  axinfndlem1  10639  axinfnd  10640  axacndlem4  10644  axacndlem5  10645  axacnd  10646  iota5f  36386  axtcond  37164  mh-setindnd  37223  bj-axreprepsep  37887  exrecfnlem  38198  wl-equsald  38367  wl-equsaldv  38368  wl-sbnf1  38383  wl-2sb6d  38386  wl-sbalnae  38390  wl-mo2df  38398  wl-eudf  38400  ax12eq  39879  ax12el  39880  ax12v2-o  39887  unielss  44124  permaxrep  45894  permaxsep  45895  alsbid  50796