Theorem albidv 1872

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

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

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 1495  ax-gen 1497  ax-17 1574

This theorem depends on definitions:  df-bi 117

This theorem is referenced by:  ax11v  1875  2albidv  1915  sbal1yz  2054  eujust  2081  euf  2084  mo23  2121  axext3  2214  bm1.1  2216  eqeq1  2238  cbvabw  2354  nfceqdf  2373  ralbidv2  2534  alexeq  2932  pm13.183  2944  eqeu  2976  mo2icl  2985  euind  2993  reuind  3011  cdeqal  3020  sbcal  3083  sbcalg  3084  sbcabel  3114  csbcow  3138  csbiebg  3170  ssconb  3340  reldisj  3546  sbcssg  3603  elint  3934  axsep2  4208  zfauscl  4209  bm1.3ii  4210  exmidel  4295  euotd  4347  freq1  4441  freq2  4443  eusv1  4549  ontr2exmid  4623  regexmid  4633  tfisi  4685  nnregexmid  4719  iota5  5308  sbcfung  5350  funimass4  5696  dffo3  5794  eufnfv  5885  dff13  5909  uchoice  6300  tfr1onlemsucfn  6506  tfr1onlemsucaccv  6507  tfr1onlembxssdm  6509  tfr1onlembfn  6510  tfrcllemsucfn  6519  tfrcllemsucaccv  6520  tfrcllembxssdm  6522  tfrcllembfn  6523  tfrcl  6530  frecabcl  6565  modom  6994  ssfiexmid  7063  ssfiexmidt  7065  domfiexmid  7067  diffitest  7076  findcard  7077  findcard2  7078  findcard2s  7079  fiintim  7123  fisseneq  7127  isomni  7335  isomnimap  7336  ismkv  7352  ismkvmap  7353  iswomni  7364  iswomnimap  7365  omniwomnimkv  7366  exmidfodomrlemr  7413  exmidfodomrlemrALT  7414  fz1sbc  10331  frecuzrdgtcl  10675  frecuzrdgfunlem  10682  zfz1iso  11106  istopg  14742  bdsep2  16532  bdsepnfALT  16535  bdzfauscl  16536  bdbm1.3ii  16537  bj-2inf  16584  bj-nn0sucALT  16624  sscoll2  16634