Theorem albidv 1877

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

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

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 1500  ax-gen 1502  ax-17 1579

This theorem depends on definitions:  df-bi 117

This theorem is referenced by:  ax11v  1880  2albidv  1920  sbal1yz  2061  eujust  2088  euf  2091  mo23  2128  axext3  2221  bm1.1  2223  eqeq1  2245  cbvabw  2363  nfceqdf  2391  ralbidv2  2552  alexeq  2952  pm13.183  2964  eqeu  2996  mo2icl  3005  euind  3013  reuind  3031  cdeqal  3040  sbcal  3103  sbcalg  3104  sbcabel  3134  csbcow  3158  csbiebg  3190  ssconb  3362  reldisj  3575  sbcssg  3633  elint  3971  axsepg  4245  sepg  4246  zfausclOLD  4248  bm1.3ii  4249  exmidel  4337  euotd  4390  freq1  4484  freq2  4486  eusv1  4593  ontr2exmid  4667  regexmid  4677  tfisi  4729  nnregexmid  4763  iota5  5354  sbcfung  5396  funimass4  5747  dffo3  5846  eufnfv  5939  dff13  5964  uchoice  6361  tfr1onlemsucfn  6601  tfr1onlemsucaccv  6602  tfr1onlembxssdm  6604  tfr1onlembfn  6605  tfrcllemsucfn  6614  tfrcllemsucaccv  6615  tfrcllembxssdm  6617  tfrcllembfn  6618  tfrcl  6625  frecabcl  6660  modom  7098  ssfiexmid  7168  ssfiexmidt  7170  domfiexmid  7172  diffitest  7181  findcard  7182  findcard2  7183  findcard2s  7184  fiintim  7228  fisseneq  7232  isomni  7466  isomnimap  7467  ismkv  7483  ismkvmap  7484  iswomni  7495  iswomnimap  7496  omniwomnimkv  7497  exmidfodomrlemr  7544  exmidfodomrlemrALT  7545  fz1sbc  10481  frecuzrdgtcl  10827  frecuzrdgfunlem  10834  zfz1iso  11271  istopg  15023  bdsep2  16826  bdsepnfALT  16829  bdsepg  16830  bdbm1.3ii  16831  bj-2inf  16878  bj-nn0sucALT  16918  sscoll2  16928