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  2929  pm13.183  2941  eqeu  2973  mo2icl  2982  euind  2990  reuind  3008  cdeqal  3017  sbcal  3080  sbcalg  3081  sbcabel  3111  csbcow  3135  csbiebg  3167  ssconb  3337  reldisj  3543  sbcssg  3600  elint  3929  axsep2  4203  zfauscl  4204  bm1.3ii  4205  exmidel  4289  euotd  4341  freq1  4435  freq2  4437  eusv1  4543  ontr2exmid  4617  regexmid  4627  tfisi  4679  nnregexmid  4713  iota5  5300  sbcfung  5342  funimass4  5684  dffo3  5782  eufnfv  5870  dff13  5892  uchoice  6283  tfr1onlemsucfn  6486  tfr1onlemsucaccv  6487  tfr1onlembxssdm  6489  tfr1onlembfn  6490  tfrcllemsucfn  6499  tfrcllemsucaccv  6500  tfrcllembxssdm  6502  tfrcllembfn  6503  tfrcl  6510  frecabcl  6545  ssfiexmid  7038  domfiexmid  7040  diffitest  7049  findcard  7050  findcard2  7051  findcard2s  7052  fiintim  7093  fisseneq  7096  isomni  7303  isomnimap  7304  ismkv  7320  ismkvmap  7321  iswomni  7332  iswomnimap  7333  omniwomnimkv  7334  exmidfodomrlemr  7380  exmidfodomrlemrALT  7381  fz1sbc  10292  frecuzrdgtcl  10634  frecuzrdgfunlem  10641  zfz1iso  11063  istopg  14673  bdsep2  16249  bdsepnfALT  16252  bdzfauscl  16253  bdbm1.3ii  16254  bj-2inf  16301  bj-nn0sucALT  16341  sscoll2  16351