Theorem albid 2255

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

Syntax hints:   → wi 4   ↔ wb 197  ∀wal 1650  Ⅎwnf 1878

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1890  ax-4 1904  ax-5 2005  ax-6 2069  ax-7 2105  ax-12 2211

This theorem depends on definitions:  df-bi 198  df-ex 1875  df-nf 1879

This theorem is referenced by:  nfbidf  2257  axc15  2403  dral2  2418  dral1  2419  sbal1  2552  sbal2  2553  mobid  2580  eubidOLD  2617  ralbida  3129  raleqf  3282  intab  4663  fin23lem32  9419  axrepndlem1  9667  axrepndlem2  9668  axrepnd  9669  axunnd  9671  axpowndlem2  9673  axpowndlem4  9675  axregndlem2  9678  axinfndlem1  9680  axinfnd  9681  axacndlem4  9685  axacndlem5  9686  axacnd  9687  iota5f  31984  bj-dral1v  33114  wl-equsald  33682  wl-sbnf1  33694  wl-2sb6d  33698  wl-sbalnae  33702  wl-mo2df  33709  wl-eudf  33711  wl-ax11-lem6  33724  wl-ax11-lem8  33726  ax12eq  34829  ax12el  34830  ax12v2-o  34837