Theorem albidv 1812

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

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

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 1435  ax-gen 1437  ax-17 1514

This theorem depends on definitions:  df-bi 116

This theorem is referenced by:  ax11v  1815  2albidv  1855  sbal1yz  1989  eujust  2016  euf  2019  mo23  2055  axext3  2148  bm1.1  2150  eqeq1  2172  cbvabw  2289  nfceqdf  2307  ralbidv2  2468  alexeq  2852  pm13.183  2864  eqeu  2896  mo2icl  2905  euind  2913  reuind  2931  cdeqal  2940  sbcal  3002  sbcalg  3003  sbcabel  3032  csbcow  3056  csbiebg  3087  ssconb  3255  reldisj  3460  sbcssg  3518  elint  3830  axsep2  4101  zfauscl  4102  bm1.3ii  4103  exmidel  4184  euotd  4232  freq1  4322  freq2  4324  eusv1  4430  ontr2exmid  4502  regexmid  4512  tfisi  4564  nnregexmid  4598  iota5  5173  sbcfung  5212  funimass4  5537  dffo3  5632  eufnfv  5715  dff13  5736  tfr1onlemsucfn  6308  tfr1onlemsucaccv  6309  tfr1onlembxssdm  6311  tfr1onlembfn  6312  tfrcllemsucfn  6321  tfrcllemsucaccv  6322  tfrcllembxssdm  6324  tfrcllembfn  6325  tfrcl  6332  frecabcl  6367  ssfiexmid  6842  domfiexmid  6844  diffitest  6853  findcard  6854  findcard2  6855  findcard2s  6856  fiintim  6894  fisseneq  6897  isomni  7100  isomnimap  7101  ismkv  7117  ismkvmap  7118  iswomni  7129  iswomnimap  7130  omniwomnimkv  7131  exmidfodomrlemr  7158  exmidfodomrlemrALT  7159  fz1sbc  10031  frecuzrdgtcl  10347  frecuzrdgfunlem  10354  zfz1iso  10754  istopg  12637  bdsep2  13768  bdsepnfALT  13771  bdzfauscl  13772  bdbm1.3ii  13773  bj-2inf  13820  bj-nn0sucALT  13860  sscoll2  13870