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

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

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 1495  ax-gen 1497  ax-17 1574

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  2354  nfceqdf  2373  ralbidv2  2534  alexeq  2932  pm13.183  2944  eqeu  2976  mo2icl  2985  euind  2993  reuind  3011  cdeqal  3020  sbcal  3083  sbcalg  3084  sbcabel  3114  csbcow  3138  csbiebg  3170  ssconb  3340  reldisj  3546  sbcssg  3603  elint  3934  axsep2  4208  zfauscl  4209  bm1.3ii  4210  exmidel  4295  euotd  4347  freq1  4441  freq2  4443  eusv1  4549  ontr2exmid  4623  regexmid  4633  tfisi  4685  nnregexmid  4719  iota5  5308  sbcfung  5350  funimass4  5696  dffo3  5794  eufnfv  5884  dff13  5908  uchoice  6299  tfr1onlemsucfn  6505  tfr1onlemsucaccv  6506  tfr1onlembxssdm  6508  tfr1onlembfn  6509  tfrcllemsucfn  6518  tfrcllemsucaccv  6519  tfrcllembxssdm  6521  tfrcllembfn  6522  tfrcl  6529  frecabcl  6564  modom  6993  ssfiexmid  7062  ssfiexmidt  7064  domfiexmid  7066  diffitest  7075  findcard  7076  findcard2  7077  findcard2s  7078  fiintim  7122  fisseneq  7126  isomni  7334  isomnimap  7335  ismkv  7351  ismkvmap  7352  iswomni  7363  iswomnimap  7364  omniwomnimkv  7365  exmidfodomrlemr  7412  exmidfodomrlemrALT  7413  fz1sbc  10330  frecuzrdgtcl  10673  frecuzrdgfunlem  10680  zfz1iso  11104  istopg  14722  bdsep2  16481  bdsepnfALT  16484  bdzfauscl  16485  bdbm1.3ii  16486  bj-2inf  16533  bj-nn0sucALT  16573  sscoll2  16583