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  6616  tfr1onlemsucaccv  6617  tfr1onlembxssdm  6619  tfr1onlembfn  6620  tfrcllemsucfn  6629  tfrcllemsucaccv  6630  tfrcllembxssdm  6632  tfrcllembfn  6633  tfrcl  6640  frecabcl  6675  modom  7114  ssfiexmid  7184  ssfiexmidt  7186  domfiexmid  7188  diffitest  7197  findcard  7198  findcard2  7199  findcard2s  7200  fiintim  7244  fisseneq  7248  isomni  7482  isomnimap  7483  ismkv  7499  ismkvmap  7500  iswomni  7511  iswomnimap  7512  omniwomnimkv  7513  exmidfodomrlemr  7560  exmidfodomrlemrALT  7561  fz1sbc  10519  frecuzrdgtcl  10869  frecuzrdgfunlem  10876  zfz1iso  11314  istopg  15242  bdsep2  17134  bdsepnfALT  17137  bdsepg  17138  bdbm1.3ii  17139  bj-2inf  17186  bj-nn0sucALT  17226  sscoll2  17236  wexmiddiffilem  17265  wexmiddifxy  17268