Theorem albidv 1872

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

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

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 1496  ax-gen 1498  ax-17 1575

This theorem depends on definitions:  df-bi 117

This theorem is referenced by:  ax11v  1875  2albidv  1915  sbal1yz  2054  eujust  2081  euf  2084  mo23  2121  axext3  2214  bm1.1  2216  eqeq1  2238  cbvabw  2355  nfceqdf  2374  ralbidv2  2535  alexeq  2933  pm13.183  2945  eqeu  2977  mo2icl  2986  euind  2994  reuind  3012  cdeqal  3021  sbcal  3084  sbcalg  3085  sbcabel  3115  csbcow  3139  csbiebg  3171  ssconb  3342  reldisj  3548  sbcssg  3605  elint  3939  axsep2  4213  zfauscl  4214  bm1.3ii  4215  exmidel  4301  euotd  4353  freq1  4447  freq2  4449  eusv1  4555  ontr2exmid  4629  regexmid  4639  tfisi  4691  nnregexmid  4725  iota5  5315  sbcfung  5357  funimass4  5705  dffo3  5802  eufnfv  5895  dff13  5919  uchoice  6309  tfr1onlemsucfn  6549  tfr1onlemsucaccv  6550  tfr1onlembxssdm  6552  tfr1onlembfn  6553  tfrcllemsucfn  6562  tfrcllemsucaccv  6563  tfrcllembxssdm  6565  tfrcllembfn  6566  tfrcl  6573  frecabcl  6608  modom  7037  ssfiexmid  7106  ssfiexmidt  7108  domfiexmid  7110  diffitest  7119  findcard  7120  findcard2  7121  findcard2s  7122  fiintim  7166  fisseneq  7170  isomni  7395  isomnimap  7396  ismkv  7412  ismkvmap  7413  iswomni  7424  iswomnimap  7425  omniwomnimkv  7426  exmidfodomrlemr  7473  exmidfodomrlemrALT  7474  fz1sbc  10393  frecuzrdgtcl  10737  frecuzrdgfunlem  10744  zfz1iso  11168  istopg  14810  bdsep2  16602  bdsepnfALT  16605  bdzfauscl  16606  bdbm1.3ii  16607  bj-2inf  16654  bj-nn0sucALT  16694  sscoll2  16704