Theorem albidv 1847

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

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

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 1470  ax-gen 1472  ax-17 1549

This theorem depends on definitions:  df-bi 117

This theorem is referenced by:  ax11v  1850  2albidv  1890  sbal1yz  2029  eujust  2056  euf  2059  mo23  2095  axext3  2188  bm1.1  2190  eqeq1  2212  cbvabw  2328  nfceqdf  2347  ralbidv2  2508  alexeq  2899  pm13.183  2911  eqeu  2943  mo2icl  2952  euind  2960  reuind  2978  cdeqal  2987  sbcal  3050  sbcalg  3051  sbcabel  3080  csbcow  3104  csbiebg  3136  ssconb  3306  reldisj  3512  sbcssg  3569  elint  3891  axsep2  4163  zfauscl  4164  bm1.3ii  4165  exmidel  4249  euotd  4299  freq1  4391  freq2  4393  eusv1  4499  ontr2exmid  4573  regexmid  4583  tfisi  4635  nnregexmid  4669  iota5  5253  sbcfung  5295  funimass4  5629  dffo3  5727  eufnfv  5815  dff13  5837  uchoice  6223  tfr1onlemsucfn  6426  tfr1onlemsucaccv  6427  tfr1onlembxssdm  6429  tfr1onlembfn  6430  tfrcllemsucfn  6439  tfrcllemsucaccv  6440  tfrcllembxssdm  6442  tfrcllembfn  6443  tfrcl  6450  frecabcl  6485  ssfiexmid  6973  domfiexmid  6975  diffitest  6984  findcard  6985  findcard2  6986  findcard2s  6987  fiintim  7028  fisseneq  7031  isomni  7238  isomnimap  7239  ismkv  7255  ismkvmap  7256  iswomni  7267  iswomnimap  7268  omniwomnimkv  7269  exmidfodomrlemr  7310  exmidfodomrlemrALT  7311  fz1sbc  10218  frecuzrdgtcl  10557  frecuzrdgfunlem  10564  zfz1iso  10986  istopg  14471  bdsep2  15822  bdsepnfALT  15825  bdzfauscl  15826  bdbm1.3ii  15827  bj-2inf  15874  bj-nn0sucALT  15914  sscoll2  15924