Theorem albidv 1797

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

Syntax hints:   -> wi 4   <-> wb 104   A.wal 1330

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-5 1424  ax-gen 1426  ax-17 1507

This theorem depends on definitions:  df-bi 116

This theorem is referenced by:  ax11v  1800  2albidv  1840  sbal1yz  1977  eujust  2002  euf  2005  mo23  2041  axext3  2123  bm1.1  2125  eqeq1  2147  nfceqdf  2281  ralbidv2  2440  alexeq  2815  pm13.183  2826  eqeu  2858  mo2icl  2867  euind  2875  reuind  2893  cdeqal  2902  sbcal  2964  sbcalg  2965  sbcabel  2994  csbiebg  3047  ssconb  3214  reldisj  3419  sbcssg  3477  elint  3785  axsep2  4055  zfauscl  4056  bm1.3ii  4057  exmidel  4136  euotd  4184  freq1  4274  freq2  4276  eusv1  4381  ontr2exmid  4448  regexmid  4458  tfisi  4509  nnregexmid  4542  iota5  5116  sbcfung  5155  funimass4  5480  dffo3  5575  eufnfv  5656  dff13  5677  tfr1onlemsucfn  6245  tfr1onlemsucaccv  6246  tfr1onlembxssdm  6248  tfr1onlembfn  6249  tfrcllemsucfn  6258  tfrcllemsucaccv  6259  tfrcllembxssdm  6261  tfrcllembfn  6262  tfrcl  6269  frecabcl  6304  ssfiexmid  6778  domfiexmid  6780  diffitest  6789  findcard  6790  findcard2  6791  findcard2s  6792  fiintim  6825  fisseneq  6828  isomni  7016  isomnimap  7017  ismkv  7035  ismkvmap  7036  iswomni  7047  iswomnimap  7048  omniwomnimkv  7049  exmidfodomrlemr  7075  exmidfodomrlemrALT  7076  fz1sbc  9907  frecuzrdgtcl  10216  frecuzrdgfunlem  10223  zfz1iso  10616  istopg  12205  bdsep2  13255  bdsepnfALT  13258  bdzfauscl  13259  bdbm1.3ii  13260  bj-2inf  13307  bj-nn0sucALT  13347  sscoll2  13357