Theorem albidv 1877

Description: Formula-building rule for universal quantifier (deduction form). (Contributed by NM, 5-Aug-1993.)

Hypothesis

Ref	Expression
albidv.1	|- ( ph -> ( ps <-> ch ) )

Assertion

Ref	Expression
albidv	|- ( ph -> ( A. x ps <-> A. x ch ) )

Distinct variable group:   ph, x

Allowed substitution hints:   ps( x)   ch( x)

Proof of Theorem albidv

Step	Hyp	Ref	Expression
1		ax-17 1579	. 2 |- ( ph -> A. x ph )
2		albidv.1	. 2 |- ( ph -> ( ps <-> ch ) )
3	1, 2	albidh 1533	1 |- ( ph -> ( A. x ps <-> A. x ch ) )

This proof depends on syntax axioms:   -> wi 4   <-> wb 105   A.wal 1400

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-5 1500  ax-gen 1502  ax-17 1579

This proof depends on definitions:  df-bi 117

This theorem is used by:  ax11v  1880  2albidv  1920  sbal1yz  2061  eujust  2088  euf  2091  mo23  2128  axext3  2221  bm1.1  2223  eqeq1  2245  cbvabw  2363  nfceqdf  2391  ralbidv2  2552  alexeq  2952  pm13.183  2964  eqeu  2996  mo2icl  3005  euind  3013  reuind  3031  cdeqal  3040  sbcal  3103  sbcalg  3104  sbcabel  3134  csbcow  3158  csbiebg  3190  ssconb  3362  reldisj  3576  sbcssg  3636  elint  3976  axsepg  4252  sepg  4253  zfausclOLD  4255  bm1.3ii  4256  exmidel  4344  euotd  4397  freq1  4491  freq2  4493  eusv1  4600  ontr2exmid  4674  regexmid  4684  tfisi  4736  nnregexmid  4770  iota5  5362  sbcfung  5404  funimass4  5756  dffo3  5858  eufnfv  5952  dff13  5977  uchoice  6375  tfr1onlemsucfn  6615  tfr1onlemsucaccv  6616  tfr1onlembxssdm  6618  tfr1onlembfn  6619  tfrcllemsucfn  6628  tfrcllemsucaccv  6629  tfrcllembxssdm  6631  tfrcllembfn  6632  tfrcl  6639  frecabcl  6674  modom  7112  ssfiexmid  7182  ssfiexmidt  7184  domfiexmid  7186  diffitest  7195  findcard  7196  findcard2  7197  findcard2s  7198  fiintim  7242  fisseneq  7246  isomni  7482  isomnimap  7483  ismkv  7499  ismkvmap  7500  iswomni  7511  iswomnimap  7512  omniwomnimkv  7513  exmidfodomrlemr  7560  exmidfodomrlemrALT  7561  fz1sbc  10520  frecuzrdgtcl  10870  frecuzrdgfunlem  10877  zfz1iso  11315  istopg  15225  bdsep2  17117  bdsepnfALT  17120  bdsepg  17121  bdbm1.3ii  17122  bj-2inf  17169  bj-nn0sucALT  17209  sscoll2  17219  wexmiddiffilem  17248  wexmiddifxy  17251