Theorem albid 2188

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

Syntax hints:   → wi 4   ↔ wb 207  ∀wal 1520  Ⅎwnf 1766

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1778  ax-4 1792  ax-5 1889  ax-6 1948  ax-7 1993  ax-12 2140

This theorem depends on definitions:  df-bi 208  df-ex 1763  df-nf 1767

This theorem is referenced by:  nfbidf  2190  axc15OLD  2400  dral2  2416  dral1  2417  sb4b  2456  sbal1  2524  sbal2  2525  sbal2OLD  2526  sbal2OLDOLD  2527  mobidOLD  2589  ralbida  3193  raleqf  3356  intab  4814  fin23lem32  9615  axrepndlem1  9863  axrepndlem2  9864  axrepnd  9865  axunnd  9867  axpowndlem2  9869  axpowndlem4  9871  axregndlem2  9874  axinfndlem1  9876  axinfnd  9877  axacndlem4  9881  axacndlem5  9882  axacnd  9883  iota5f  32557  bj-dral1v  33677  exrecfnlem  34204  wl-equsald  34324  wl-sbnf1  34335  wl-2sb6d  34338  wl-sbalnae  34342  wl-mo2df  34350  wl-eudf  34352  wl-ax11-lem6  34366  wl-ax11-lem8  34368  wl-dfrmof  34399  ax12eq  35621  ax12el  35622  ax12v2-o  35629