Theorem albidv 1846

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 1548	. 2 ⊢ (𝜑 → ∀𝑥𝜑)
2		albidv.1	. 2 ⊢ (𝜑 → (𝜓 ↔ 𝜒))
3	1, 2	albidh 1502	1 ⊢ (𝜑 → (∀𝑥𝜓 ↔ ∀𝑥𝜒))

Syntax hints:   → wi 4   ↔ wb 105  ∀wal 1370

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-5 1469  ax-gen 1471  ax-17 1548

This theorem depends on definitions:  df-bi 117

This theorem is referenced by:  ax11v  1849  2albidv  1889  sbal1yz  2028  eujust  2055  euf  2058  mo23  2094  axext3  2187  bm1.1  2189  eqeq1  2211  cbvabw  2327  nfceqdf  2346  ralbidv2  2507  alexeq  2898  pm13.183  2910  eqeu  2942  mo2icl  2951  euind  2959  reuind  2977  cdeqal  2986  sbcal  3049  sbcalg  3050  sbcabel  3079  csbcow  3103  csbiebg  3135  ssconb  3305  reldisj  3511  sbcssg  3568  elint  3890  axsep2  4162  zfauscl  4163  bm1.3ii  4164  exmidel  4248  euotd  4298  freq1  4390  freq2  4392  eusv1  4498  ontr2exmid  4572  regexmid  4582  tfisi  4634  nnregexmid  4668  iota5  5252  sbcfung  5294  funimass4  5628  dffo3  5726  eufnfv  5814  dff13  5836  uchoice  6222  tfr1onlemsucfn  6425  tfr1onlemsucaccv  6426  tfr1onlembxssdm  6428  tfr1onlembfn  6429  tfrcllemsucfn  6438  tfrcllemsucaccv  6439  tfrcllembxssdm  6441  tfrcllembfn  6442  tfrcl  6449  frecabcl  6484  ssfiexmid  6972  domfiexmid  6974  diffitest  6983  findcard  6984  findcard2  6985  findcard2s  6986  fiintim  7027  fisseneq  7030  isomni  7237  isomnimap  7238  ismkv  7254  ismkvmap  7255  iswomni  7266  iswomnimap  7267  omniwomnimkv  7268  exmidfodomrlemr  7309  exmidfodomrlemrALT  7310  fz1sbc  10217  frecuzrdgtcl  10555  frecuzrdgfunlem  10562  zfz1iso  10984  istopg  14442  bdsep2  15784  bdsepnfALT  15787  bdzfauscl  15788  bdbm1.3ii  15789  bj-2inf  15836  bj-nn0sucALT  15876  sscoll2  15886