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  10374  frecuzrdgtcl  10718  frecuzrdgfunlem  10725  zfz1iso  11149  istopg  14790  bdsep2  16579  bdsepnfALT  16582  bdzfauscl  16583  bdbm1.3ii  16584  bj-2inf  16631  bj-nn0sucALT  16671  sscoll2  16681