Theorem albidv 1838

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

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

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 1461  ax-gen 1463  ax-17 1540

This theorem depends on definitions:  df-bi 117

This theorem is referenced by:  ax11v  1841  2albidv  1881  sbal1yz  2020  eujust  2047  euf  2050  mo23  2086  axext3  2179  bm1.1  2181  eqeq1  2203  cbvabw  2319  nfceqdf  2338  ralbidv2  2499  alexeq  2890  pm13.183  2902  eqeu  2934  mo2icl  2943  euind  2951  reuind  2969  cdeqal  2978  sbcal  3041  sbcalg  3042  sbcabel  3071  csbcow  3095  csbiebg  3127  ssconb  3297  reldisj  3503  sbcssg  3560  elint  3881  axsep2  4153  zfauscl  4154  bm1.3ii  4155  exmidel  4239  euotd  4288  freq1  4380  freq2  4382  eusv1  4488  ontr2exmid  4562  regexmid  4572  tfisi  4624  nnregexmid  4658  iota5  5241  sbcfung  5283  funimass4  5614  dffo3  5712  eufnfv  5796  dff13  5818  uchoice  6204  tfr1onlemsucfn  6407  tfr1onlemsucaccv  6408  tfr1onlembxssdm  6410  tfr1onlembfn  6411  tfrcllemsucfn  6420  tfrcllemsucaccv  6421  tfrcllembxssdm  6423  tfrcllembfn  6424  tfrcl  6431  frecabcl  6466  ssfiexmid  6946  domfiexmid  6948  diffitest  6957  findcard  6958  findcard2  6959  findcard2s  6960  fiintim  7001  fisseneq  7004  isomni  7211  isomnimap  7212  ismkv  7228  ismkvmap  7229  iswomni  7240  iswomnimap  7241  omniwomnimkv  7242  exmidfodomrlemr  7281  exmidfodomrlemrALT  7282  fz1sbc  10188  frecuzrdgtcl  10521  frecuzrdgfunlem  10528  zfz1iso  10950  istopg  14319  bdsep2  15616  bdsepnfALT  15619  bdzfauscl  15620  bdbm1.3ii  15621  bj-2inf  15668  bj-nn0sucALT  15708  sscoll2  15718