Theorem albidv 1872

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

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

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 1496  ax-gen 1498  ax-17 1575

This theorem depends on definitions:  df-bi 117

This theorem is referenced by:  ax11v  1875  2albidv  1915  sbal1yz  2054  eujust  2081  euf  2084  mo23  2121  axext3  2214  bm1.1  2216  eqeq1  2238  cbvabw  2355  nfceqdf  2374  ralbidv2  2535  alexeq  2933  pm13.183  2945  eqeu  2977  mo2icl  2986  euind  2994  reuind  3012  cdeqal  3021  sbcal  3084  sbcalg  3085  sbcabel  3115  csbcow  3139  csbiebg  3171  ssconb  3342  reldisj  3548  sbcssg  3605  elint  3939  axsep2  4213  zfauscl  4214  bm1.3ii  4215  exmidel  4301  euotd  4353  freq1  4447  freq2  4449  eusv1  4555  ontr2exmid  4629  regexmid  4639  tfisi  4691  nnregexmid  4725  iota5  5315  sbcfung  5357  funimass4  5705  dffo3  5802  eufnfv  5895  dff13  5919  uchoice  6309  tfr1onlemsucfn  6549  tfr1onlemsucaccv  6550  tfr1onlembxssdm  6552  tfr1onlembfn  6553  tfrcllemsucfn  6562  tfrcllemsucaccv  6563  tfrcllembxssdm  6565  tfrcllembfn  6566  tfrcl  6573  frecabcl  6608  modom  7037  ssfiexmid  7106  ssfiexmidt  7108  domfiexmid  7110  diffitest  7119  findcard  7120  findcard2  7121  findcard2s  7122  fiintim  7166  fisseneq  7170  isomni  7378  isomnimap  7379  ismkv  7395  ismkvmap  7396  iswomni  7407  iswomnimap  7408  omniwomnimkv  7409  exmidfodomrlemr  7456  exmidfodomrlemrALT  7457  fz1sbc  10376  frecuzrdgtcl  10720  frecuzrdgfunlem  10727  zfz1iso  11151  istopg  14793  bdsep2  16585  bdsepnfALT  16588  bdzfauscl  16589  bdbm1.3ii  16590  bj-2inf  16637  bj-nn0sucALT  16677  sscoll2  16687