Theorem albidv 1796

Description: Formula-building rule for universal quantifier (deduction form). (Contributed by NM, 5-Aug-1993.)

Hypothesis

Ref	Expression
albidv.1	⊢ (𝜑 → (𝜓 ↔ 𝜒))

Assertion

Ref	Expression
albidv	⊢ (𝜑 → (∀𝑥𝜓 ↔ ∀𝑥𝜒))

Distinct variable group:   𝜑,𝑥

Allowed substitution hints:   𝜓(𝑥)   𝜒(𝑥)

Proof of Theorem albidv

Step	Hyp	Ref	Expression
1		ax-17 1506	. 2 ⊢ (𝜑 → ∀𝑥𝜑)
2		albidv.1	. 2 ⊢ (𝜑 → (𝜓 ↔ 𝜒))
3	1, 2	albidh 1456	1 ⊢ (𝜑 → (∀𝑥𝜓 ↔ ∀𝑥𝜒))

Syntax hints:   → wi 4   ↔ wb 104  ∀wal 1329

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-5 1423  ax-gen 1425  ax-17 1506

This theorem depends on definitions:  df-bi 116

This theorem is referenced by:  ax11v  1799  2albidv  1839  sbal1yz  1976  eujust  2001  euf  2004  mo23  2040  axext3  2122  bm1.1  2124  eqeq1  2146  nfceqdf  2280  ralbidv2  2439  alexeq  2811  pm13.183  2822  eqeu  2854  mo2icl  2863  euind  2871  reuind  2889  cdeqal  2898  sbcal  2960  sbcalg  2961  sbcabel  2990  csbiebg  3042  ssconb  3209  reldisj  3414  sbcssg  3472  elint  3777  axsep2  4047  zfauscl  4048  bm1.3ii  4049  exmidel  4128  euotd  4176  freq1  4266  freq2  4268  eusv1  4373  ontr2exmid  4440  regexmid  4450  tfisi  4501  nnregexmid  4534  iota5  5108  sbcfung  5147  funimass4  5472  dffo3  5567  eufnfv  5648  dff13  5669  tfr1onlemsucfn  6237  tfr1onlemsucaccv  6238  tfr1onlembxssdm  6240  tfr1onlembfn  6241  tfrcllemsucfn  6250  tfrcllemsucaccv  6251  tfrcllembxssdm  6253  tfrcllembfn  6254  tfrcl  6261  frecabcl  6296  ssfiexmid  6770  domfiexmid  6772  diffitest  6781  findcard  6782  findcard2  6783  findcard2s  6784  fiintim  6817  fisseneq  6820  isomni  7008  isomnimap  7009  ismkv  7027  ismkvmap  7028  exmidfodomrlemr  7058  exmidfodomrlemrALT  7059  fz1sbc  9876  frecuzrdgtcl  10185  frecuzrdgfunlem  10192  zfz1iso  10584  istopg  12166  bdsep2  13084  bdsepnfALT  13087  bdzfauscl  13088  bdbm1.3ii  13089  bj-2inf  13136  bj-nn0sucALT  13176  strcoll2  13181  strcollnfALT  13184