Theorem albidv 1870

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

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

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 1493  ax-gen 1495  ax-17 1572

This theorem depends on definitions:  df-bi 117

This theorem is referenced by:  ax11v  1873  2albidv  1913  sbal1yz  2052  eujust  2079  euf  2082  mo23  2119  axext3  2212  bm1.1  2214  eqeq1  2236  cbvabw  2352  nfceqdf  2371  ralbidv2  2532  alexeq  2930  pm13.183  2942  eqeu  2974  mo2icl  2983  euind  2991  reuind  3009  cdeqal  3018  sbcal  3081  sbcalg  3082  sbcabel  3112  csbcow  3136  csbiebg  3168  ssconb  3338  reldisj  3544  sbcssg  3601  elint  3932  axsep2  4206  zfauscl  4207  bm1.3ii  4208  exmidel  4293  euotd  4345  freq1  4439  freq2  4441  eusv1  4547  ontr2exmid  4621  regexmid  4631  tfisi  4683  nnregexmid  4717  iota5  5306  sbcfung  5348  funimass4  5692  dffo3  5790  eufnfv  5880  dff13  5904  uchoice  6295  tfr1onlemsucfn  6501  tfr1onlemsucaccv  6502  tfr1onlembxssdm  6504  tfr1onlembfn  6505  tfrcllemsucfn  6514  tfrcllemsucaccv  6515  tfrcllembxssdm  6517  tfrcllembfn  6518  tfrcl  6525  frecabcl  6560  modom  6989  ssfiexmid  7058  domfiexmid  7060  diffitest  7069  findcard  7070  findcard2  7071  findcard2s  7072  fiintim  7116  fisseneq  7119  isomni  7326  isomnimap  7327  ismkv  7343  ismkvmap  7344  iswomni  7355  iswomnimap  7356  omniwomnimkv  7357  exmidfodomrlemr  7403  exmidfodomrlemrALT  7404  fz1sbc  10321  frecuzrdgtcl  10664  frecuzrdgfunlem  10671  zfz1iso  11095  istopg  14713  bdsep2  16417  bdsepnfALT  16420  bdzfauscl  16421  bdbm1.3ii  16422  bj-2inf  16469  bj-nn0sucALT  16509  sscoll2  16519