Theorem albidv 1835

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

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

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 1458  ax-gen 1460  ax-17 1537

This theorem depends on definitions:  df-bi 117

This theorem is referenced by:  ax11v  1838  2albidv  1878  sbal1yz  2017  eujust  2044  euf  2047  mo23  2083  axext3  2176  bm1.1  2178  eqeq1  2200  cbvabw  2316  nfceqdf  2335  ralbidv2  2496  alexeq  2886  pm13.183  2898  eqeu  2930  mo2icl  2939  euind  2947  reuind  2965  cdeqal  2974  sbcal  3037  sbcalg  3038  sbcabel  3067  csbcow  3091  csbiebg  3123  ssconb  3292  reldisj  3498  sbcssg  3555  elint  3876  axsep2  4148  zfauscl  4149  bm1.3ii  4150  exmidel  4234  euotd  4283  freq1  4375  freq2  4377  eusv1  4483  ontr2exmid  4557  regexmid  4567  tfisi  4619  nnregexmid  4653  iota5  5236  sbcfung  5278  funimass4  5607  dffo3  5705  eufnfv  5789  dff13  5811  uchoice  6190  tfr1onlemsucfn  6393  tfr1onlemsucaccv  6394  tfr1onlembxssdm  6396  tfr1onlembfn  6397  tfrcllemsucfn  6406  tfrcllemsucaccv  6407  tfrcllembxssdm  6409  tfrcllembfn  6410  tfrcl  6417  frecabcl  6452  ssfiexmid  6932  domfiexmid  6934  diffitest  6943  findcard  6944  findcard2  6945  findcard2s  6946  fiintim  6985  fisseneq  6988  isomni  7195  isomnimap  7196  ismkv  7212  ismkvmap  7213  iswomni  7224  iswomnimap  7225  omniwomnimkv  7226  exmidfodomrlemr  7262  exmidfodomrlemrALT  7263  fz1sbc  10162  frecuzrdgtcl  10483  frecuzrdgfunlem  10490  zfz1iso  10912  istopg  14167  bdsep2  15378  bdsepnfALT  15381  bdzfauscl  15382  bdbm1.3ii  15383  bj-2inf  15430  bj-nn0sucALT  15470  sscoll2  15480