Theorem albidv 1848

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

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

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 1471  ax-gen 1473  ax-17 1550

This theorem depends on definitions:  df-bi 117

This theorem is referenced by:  ax11v  1851  2albidv  1891  sbal1yz  2030  eujust  2057  euf  2060  mo23  2097  axext3  2190  bm1.1  2192  eqeq1  2214  cbvabw  2330  nfceqdf  2349  ralbidv2  2510  alexeq  2906  pm13.183  2918  eqeu  2950  mo2icl  2959  euind  2967  reuind  2985  cdeqal  2994  sbcal  3057  sbcalg  3058  sbcabel  3088  csbcow  3112  csbiebg  3144  ssconb  3314  reldisj  3520  sbcssg  3577  elint  3905  axsep2  4179  zfauscl  4180  bm1.3ii  4181  exmidel  4265  euotd  4317  freq1  4409  freq2  4411  eusv1  4517  ontr2exmid  4591  regexmid  4601  tfisi  4653  nnregexmid  4687  iota5  5272  sbcfung  5314  funimass4  5652  dffo3  5750  eufnfv  5838  dff13  5860  uchoice  6246  tfr1onlemsucfn  6449  tfr1onlemsucaccv  6450  tfr1onlembxssdm  6452  tfr1onlembfn  6453  tfrcllemsucfn  6462  tfrcllemsucaccv  6463  tfrcllembxssdm  6465  tfrcllembfn  6466  tfrcl  6473  frecabcl  6508  ssfiexmid  6999  domfiexmid  7001  diffitest  7010  findcard  7011  findcard2  7012  findcard2s  7013  fiintim  7054  fisseneq  7057  isomni  7264  isomnimap  7265  ismkv  7281  ismkvmap  7282  iswomni  7293  iswomnimap  7294  omniwomnimkv  7295  exmidfodomrlemr  7341  exmidfodomrlemrALT  7342  fz1sbc  10253  frecuzrdgtcl  10594  frecuzrdgfunlem  10601  zfz1iso  11023  istopg  14586  bdsep2  16021  bdsepnfALT  16024  bdzfauscl  16025  bdbm1.3ii  16026  bj-2inf  16073  bj-nn0sucALT  16113  sscoll2  16123