Theorem albidv 1817

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

Syntax hints:   → wi 4   ↔ wb 104  ∀wal 1346

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-5 1440  ax-gen 1442  ax-17 1519

This theorem depends on definitions:  df-bi 116

This theorem is referenced by:  ax11v  1820  2albidv  1860  sbal1yz  1994  eujust  2021  euf  2024  mo23  2060  axext3  2153  bm1.1  2155  eqeq1  2177  cbvabw  2293  nfceqdf  2311  ralbidv2  2472  alexeq  2856  pm13.183  2868  eqeu  2900  mo2icl  2909  euind  2917  reuind  2935  cdeqal  2944  sbcal  3006  sbcalg  3007  sbcabel  3036  csbcow  3060  csbiebg  3091  ssconb  3260  reldisj  3466  sbcssg  3524  elint  3837  axsep2  4108  zfauscl  4109  bm1.3ii  4110  exmidel  4191  euotd  4239  freq1  4329  freq2  4331  eusv1  4437  ontr2exmid  4509  regexmid  4519  tfisi  4571  nnregexmid  4605  iota5  5180  sbcfung  5222  funimass4  5547  dffo3  5643  eufnfv  5726  dff13  5747  tfr1onlemsucfn  6319  tfr1onlemsucaccv  6320  tfr1onlembxssdm  6322  tfr1onlembfn  6323  tfrcllemsucfn  6332  tfrcllemsucaccv  6333  tfrcllembxssdm  6335  tfrcllembfn  6336  tfrcl  6343  frecabcl  6378  ssfiexmid  6854  domfiexmid  6856  diffitest  6865  findcard  6866  findcard2  6867  findcard2s  6868  fiintim  6906  fisseneq  6909  isomni  7112  isomnimap  7113  ismkv  7129  ismkvmap  7130  iswomni  7141  iswomnimap  7142  omniwomnimkv  7143  exmidfodomrlemr  7179  exmidfodomrlemrALT  7180  fz1sbc  10052  frecuzrdgtcl  10368  frecuzrdgfunlem  10375  zfz1iso  10776  istopg  12791  bdsep2  13921  bdsepnfALT  13924  bdzfauscl  13925  bdbm1.3ii  13926  bj-2inf  13973  bj-nn0sucALT  14013  sscoll2  14023