Theorem albidv 1824

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

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

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 1447  ax-gen 1449  ax-17 1526

This theorem depends on definitions:  df-bi 117

This theorem is referenced by:  ax11v  1827  2albidv  1867  sbal1yz  2001  eujust  2028  euf  2031  mo23  2067  axext3  2160  bm1.1  2162  eqeq1  2184  cbvabw  2300  nfceqdf  2318  ralbidv2  2479  alexeq  2863  pm13.183  2875  eqeu  2907  mo2icl  2916  euind  2924  reuind  2942  cdeqal  2951  sbcal  3014  sbcalg  3015  sbcabel  3044  csbcow  3068  csbiebg  3099  ssconb  3268  reldisj  3474  sbcssg  3532  elint  3850  axsep2  4122  zfauscl  4123  bm1.3ii  4124  exmidel  4205  euotd  4254  freq1  4344  freq2  4346  eusv1  4452  ontr2exmid  4524  regexmid  4534  tfisi  4586  nnregexmid  4620  iota5  5198  sbcfung  5240  funimass4  5566  dffo3  5663  eufnfv  5747  dff13  5768  tfr1onlemsucfn  6340  tfr1onlemsucaccv  6341  tfr1onlembxssdm  6343  tfr1onlembfn  6344  tfrcllemsucfn  6353  tfrcllemsucaccv  6354  tfrcllembxssdm  6356  tfrcllembfn  6357  tfrcl  6364  frecabcl  6399  ssfiexmid  6875  domfiexmid  6877  diffitest  6886  findcard  6887  findcard2  6888  findcard2s  6889  fiintim  6927  fisseneq  6930  isomni  7133  isomnimap  7134  ismkv  7150  ismkvmap  7151  iswomni  7162  iswomnimap  7163  omniwomnimkv  7164  exmidfodomrlemr  7200  exmidfodomrlemrALT  7201  fz1sbc  10095  frecuzrdgtcl  10411  frecuzrdgfunlem  10418  zfz1iso  10820  istopg  13469  bdsep2  14608  bdsepnfALT  14611  bdzfauscl  14612  bdbm1.3ii  14613  bj-2inf  14660  bj-nn0sucALT  14700  sscoll2  14710