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  3929  axsep2  4203  zfauscl  4204  bm1.3ii  4205  exmidel  4289  euotd  4341  freq1  4435  freq2  4437  eusv1  4543  ontr2exmid  4617  regexmid  4627  tfisi  4679  nnregexmid  4713  iota5  5300  sbcfung  5342  funimass4  5686  dffo3  5784  eufnfv  5874  dff13  5898  uchoice  6289  tfr1onlemsucfn  6492  tfr1onlemsucaccv  6493  tfr1onlembxssdm  6495  tfr1onlembfn  6496  tfrcllemsucfn  6505  tfrcllemsucaccv  6506  tfrcllembxssdm  6508  tfrcllembfn  6509  tfrcl  6516  frecabcl  6551  ssfiexmid  7046  domfiexmid  7048  diffitest  7057  findcard  7058  findcard2  7059  findcard2s  7060  fiintim  7104  fisseneq  7107  isomni  7314  isomnimap  7315  ismkv  7331  ismkvmap  7332  iswomni  7343  iswomnimap  7344  omniwomnimkv  7345  exmidfodomrlemr  7391  exmidfodomrlemrALT  7392  fz1sbc  10304  frecuzrdgtcl  10646  frecuzrdgfunlem  10653  zfz1iso  11076  istopg  14688  bdsep2  16304  bdsepnfALT  16307  bdzfauscl  16308  bdbm1.3ii  16309  bj-2inf  16356  bj-nn0sucALT  16396  sscoll2  16406