Theorem albid 2223

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

Syntax hints:   → wi 4   ↔ wb 206  ∀wal 1538  Ⅎwnf 1783

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-12 2178

This theorem depends on definitions:  df-bi 207  df-ex 1780  df-nf 1784

This theorem is referenced by:  nfbidf  2225  dral2  2436  dral1  2437  sb4b  2473  sbal1  2526  sbal2  2527  raleqf  3318  intab  4928  fin23lem32  10238  axrepndlem1  10486  axrepndlem2  10487  axrepnd  10488  axunnd  10490  axpowndlem2  10492  axpowndlem4  10494  axregndlem2  10497  axinfndlem1  10499  axinfnd  10500  axacndlem4  10504  axacndlem5  10505  axacnd  10506  iota5f  35717  exrecfnlem  37373  wl-equsald  37533  wl-equsaldv  37534  wl-sbnf1  37549  wl-2sb6d  37552  wl-sbalnae  37556  wl-mo2df  37564  wl-eudf  37566  wl-ax11-lem6  37584  wl-ax11-lem8  37586  ax12eq  38940  ax12el  38941  ax12v2-o  38948  unielss  43211  permaxrep  45000  permaxsep  45001