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  2864  pm13.183  2876  eqeu  2908  mo2icl  2917  euind  2925  reuind  2943  cdeqal  2952  sbcal  3015  sbcalg  3016  sbcabel  3045  csbcow  3069  csbiebg  3100  ssconb  3269  reldisj  3475  sbcssg  3533  elint  3851  axsep2  4123  zfauscl  4124  bm1.3ii  4125  exmidel  4206  euotd  4255  freq1  4345  freq2  4347  eusv1  4453  ontr2exmid  4525  regexmid  4535  tfisi  4587  nnregexmid  4621  iota5  5199  sbcfung  5241  funimass4  5567  dffo3  5664  eufnfv  5748  dff13  5769  tfr1onlemsucfn  6341  tfr1onlemsucaccv  6342  tfr1onlembxssdm  6344  tfr1onlembfn  6345  tfrcllemsucfn  6354  tfrcllemsucaccv  6355  tfrcllembxssdm  6357  tfrcllembfn  6358  tfrcl  6365  frecabcl  6400  ssfiexmid  6876  domfiexmid  6878  diffitest  6887  findcard  6888  findcard2  6889  findcard2s  6890  fiintim  6928  fisseneq  6931  isomni  7134  isomnimap  7135  ismkv  7151  ismkvmap  7152  iswomni  7163  iswomnimap  7164  omniwomnimkv  7165  exmidfodomrlemr  7201  exmidfodomrlemrALT  7202  fz1sbc  10096  frecuzrdgtcl  10412  frecuzrdgfunlem  10419  zfz1iso  10821  istopg  13502  bdsep2  14641  bdsepnfALT  14644  bdzfauscl  14645  bdbm1.3ii  14646  bj-2inf  14693  bj-nn0sucALT  14733  sscoll2  14743