Theorem albidv 1753

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

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

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-5 1382  ax-gen 1384  ax-17 1465

This theorem depends on definitions:  df-bi 116

This theorem is referenced by:  ax11v  1756  2albidv  1796  sbal1yz  1926  eujust  1951  euf  1954  mo23  1990  axext3  2072  bm1.1  2074  eqeq1  2095  nfceqdf  2228  ralbidv2  2383  alexeq  2744  pm13.183  2755  eqeu  2786  mo2icl  2795  euind  2803  reuind  2821  cdeqal  2830  sbcal  2891  sbcalg  2892  sbcabel  2921  csbiebg  2971  ssconb  3134  reldisj  3338  sbcssg  3395  elint  3700  axsep2  3964  zfauscl  3965  bm1.3ii  3966  exmidel  4042  euotd  4090  freq1  4180  freq2  4182  eusv1  4287  ontr2exmid  4354  regexmid  4364  tfisi  4415  nnregexmid  4447  iota5  5013  sbcfung  5052  funimass4  5368  dffo3  5460  eufnfv  5539  dff13  5561  tfr1onlemsucfn  6119  tfr1onlemsucaccv  6120  tfr1onlembxssdm  6122  tfr1onlembfn  6123  tfrcllemsucfn  6132  tfrcllemsucaccv  6133  tfrcllembxssdm  6135  tfrcllembfn  6136  tfrcl  6143  frecabcl  6178  ssfiexmid  6646  domfiexmid  6648  diffitest  6657  findcard  6658  findcard2  6659  findcard2s  6660  fiintim  6693  fisseneq  6696  isomni  6846  isomnimap  6847  exmidfodomrlemr  6882  exmidfodomrlemrALT  6883  fz1sbc  9564  frecuzrdgtcl  9873  frecuzrdgfunlem  9880  zfz1iso  10300  istopg  11752  bdsep2  12043  bdsepnfALT  12046  bdzfauscl  12047  bdbm1.3ii  12048  bj-2inf  12099  bj-nn0sucALT  12139  strcoll2  12144  strcollnfALT  12147