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  2929  pm13.183  2941  eqeu  2973  mo2icl  2982  euind  2990  reuind  3008  cdeqal  3017  sbcal  3080  sbcalg  3081  sbcabel  3111  csbcow  3135  csbiebg  3167  ssconb  3337  reldisj  3543  sbcssg  3600  elint  3928  axsep2  4202  zfauscl  4203  bm1.3ii  4204  exmidel  4288  euotd  4340  freq1  4434  freq2  4436  eusv1  4542  ontr2exmid  4616  regexmid  4626  tfisi  4678  nnregexmid  4712  iota5  5299  sbcfung  5341  funimass4  5683  dffo3  5781  eufnfv  5869  dff13  5891  uchoice  6281  tfr1onlemsucfn  6484  tfr1onlemsucaccv  6485  tfr1onlembxssdm  6487  tfr1onlembfn  6488  tfrcllemsucfn  6497  tfrcllemsucaccv  6498  tfrcllembxssdm  6500  tfrcllembfn  6501  tfrcl  6508  frecabcl  6543  ssfiexmid  7034  domfiexmid  7036  diffitest  7045  findcard  7046  findcard2  7047  findcard2s  7048  fiintim  7089  fisseneq  7092  isomni  7299  isomnimap  7300  ismkv  7316  ismkvmap  7317  iswomni  7328  iswomnimap  7329  omniwomnimkv  7330  exmidfodomrlemr  7376  exmidfodomrlemrALT  7377  fz1sbc  10288  frecuzrdgtcl  10629  frecuzrdgfunlem  10636  zfz1iso  11058  istopg  14667  bdsep2  16207  bdsepnfALT  16210  bdzfauscl  16211  bdbm1.3ii  16212  bj-2inf  16259  bj-nn0sucALT  16299  sscoll2  16309