Theorem albidv 1870

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 1572	. 2 |- ( ph -> A. x ph )
2		albidv.1	. 2 |- ( ph -> ( ps <-> ch ) )
3	1, 2	albidh 1526	1 |- ( ph -> ( A. x ps <-> A. x ch ) )

Syntax hints:   -> wi 4   <-> wb 105   A.wal 1393

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 1493  ax-gen 1495  ax-17 1572

This theorem depends on definitions:  df-bi 117

This theorem is referenced by:  ax11v  1873  2albidv  1913  sbal1yz  2052  eujust  2079  euf  2082  mo23  2119  axext3  2212  bm1.1  2214  eqeq1  2236  cbvabw  2352  nfceqdf  2371  ralbidv2  2532  alexeq  2930  pm13.183  2942  eqeu  2974  mo2icl  2983  euind  2991  reuind  3009  cdeqal  3018  sbcal  3081  sbcalg  3082  sbcabel  3112  csbcow  3136  csbiebg  3168  ssconb  3338  reldisj  3544  sbcssg  3601  elint  3930  axsep2  4204  zfauscl  4205  bm1.3ii  4206  exmidel  4291  euotd  4343  freq1  4437  freq2  4439  eusv1  4545  ontr2exmid  4619  regexmid  4629  tfisi  4681  nnregexmid  4715  iota5  5304  sbcfung  5346  funimass4  5690  dffo3  5788  eufnfv  5878  dff13  5902  uchoice  6293  tfr1onlemsucfn  6499  tfr1onlemsucaccv  6500  tfr1onlembxssdm  6502  tfr1onlembfn  6503  tfrcllemsucfn  6512  tfrcllemsucaccv  6513  tfrcllembxssdm  6515  tfrcllembfn  6516  tfrcl  6523  frecabcl  6558  modom  6987  ssfiexmid  7056  domfiexmid  7058  diffitest  7067  findcard  7068  findcard2  7069  findcard2s  7070  fiintim  7114  fisseneq  7117  isomni  7324  isomnimap  7325  ismkv  7341  ismkvmap  7342  iswomni  7353  iswomnimap  7354  omniwomnimkv  7355  exmidfodomrlemr  7401  exmidfodomrlemrALT  7402  fz1sbc  10319  frecuzrdgtcl  10662  frecuzrdgfunlem  10669  zfz1iso  11092  istopg  14710  bdsep2  16391  bdsepnfALT  16394  bdzfauscl  16395  bdbm1.3ii  16396  bj-2inf  16443  bj-nn0sucALT  16483  sscoll2  16493