Theorem albidv 1824

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

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

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 1447  ax-gen 1449  ax-17 1526

This theorem depends on definitions:  df-bi 117

This theorem is referenced by:  ax11v  1827  2albidv  1867  sbal1yz  2001  eujust  2028  euf  2031  mo23  2067  axext3  2160  bm1.1  2162  eqeq1  2184  cbvabw  2300  nfceqdf  2318  ralbidv2  2479  alexeq  2865  pm13.183  2877  eqeu  2909  mo2icl  2918  euind  2926  reuind  2944  cdeqal  2953  sbcal  3016  sbcalg  3017  sbcabel  3046  csbcow  3070  csbiebg  3101  ssconb  3270  reldisj  3476  sbcssg  3534  elint  3852  axsep2  4124  zfauscl  4125  bm1.3ii  4126  exmidel  4207  euotd  4256  freq1  4346  freq2  4348  eusv1  4454  ontr2exmid  4526  regexmid  4536  tfisi  4588  nnregexmid  4622  iota5  5200  sbcfung  5242  funimass4  5569  dffo3  5666  eufnfv  5750  dff13  5772  tfr1onlemsucfn  6344  tfr1onlemsucaccv  6345  tfr1onlembxssdm  6347  tfr1onlembfn  6348  tfrcllemsucfn  6357  tfrcllemsucaccv  6358  tfrcllembxssdm  6360  tfrcllembfn  6361  tfrcl  6368  frecabcl  6403  ssfiexmid  6879  domfiexmid  6881  diffitest  6890  findcard  6891  findcard2  6892  findcard2s  6893  fiintim  6931  fisseneq  6934  isomni  7137  isomnimap  7138  ismkv  7154  ismkvmap  7155  iswomni  7166  iswomnimap  7167  omniwomnimkv  7168  exmidfodomrlemr  7204  exmidfodomrlemrALT  7205  fz1sbc  10099  frecuzrdgtcl  10415  frecuzrdgfunlem  10422  zfz1iso  10824  istopg  13639  bdsep2  14778  bdsepnfALT  14781  bdzfauscl  14782  bdbm1.3ii  14783  bj-2inf  14830  bj-nn0sucALT  14870  sscoll2  14880