Theorem albidv 1835

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 1537	. 2 ⊢ (𝜑 → ∀𝑥𝜑)
2		albidv.1	. 2 ⊢ (𝜑 → (𝜓 ↔ 𝜒))
3	1, 2	albidh 1491	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 1458  ax-gen 1460  ax-17 1537

This theorem depends on definitions:  df-bi 117

This theorem is referenced by:  ax11v  1838  2albidv  1878  sbal1yz  2017  eujust  2044  euf  2047  mo23  2083  axext3  2176  bm1.1  2178  eqeq1  2200  cbvabw  2316  nfceqdf  2335  ralbidv2  2496  alexeq  2887  pm13.183  2899  eqeu  2931  mo2icl  2940  euind  2948  reuind  2966  cdeqal  2975  sbcal  3038  sbcalg  3039  sbcabel  3068  csbcow  3092  csbiebg  3124  ssconb  3293  reldisj  3499  sbcssg  3556  elint  3877  axsep2  4149  zfauscl  4150  bm1.3ii  4151  exmidel  4235  euotd  4284  freq1  4376  freq2  4378  eusv1  4484  ontr2exmid  4558  regexmid  4568  tfisi  4620  nnregexmid  4654  iota5  5237  sbcfung  5279  funimass4  5608  dffo3  5706  eufnfv  5790  dff13  5812  uchoice  6192  tfr1onlemsucfn  6395  tfr1onlemsucaccv  6396  tfr1onlembxssdm  6398  tfr1onlembfn  6399  tfrcllemsucfn  6408  tfrcllemsucaccv  6409  tfrcllembxssdm  6411  tfrcllembfn  6412  tfrcl  6419  frecabcl  6454  ssfiexmid  6934  domfiexmid  6936  diffitest  6945  findcard  6946  findcard2  6947  findcard2s  6948  fiintim  6987  fisseneq  6990  isomni  7197  isomnimap  7198  ismkv  7214  ismkvmap  7215  iswomni  7226  iswomnimap  7227  omniwomnimkv  7228  exmidfodomrlemr  7264  exmidfodomrlemrALT  7265  fz1sbc  10165  frecuzrdgtcl  10486  frecuzrdgfunlem  10493  zfz1iso  10915  istopg  14178  bdsep2  15448  bdsepnfALT  15451  bdzfauscl  15452  bdbm1.3ii  15453  bj-2inf  15500  bj-nn0sucALT  15540  sscoll2  15550