Theorem albidv 1847

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

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

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 1470  ax-gen 1472  ax-17 1549

This theorem depends on definitions:  df-bi 117

This theorem is referenced by:  ax11v  1850  2albidv  1890  sbal1yz  2029  eujust  2056  euf  2059  mo23  2095  axext3  2188  bm1.1  2190  eqeq1  2212  cbvabw  2328  nfceqdf  2347  ralbidv2  2508  alexeq  2899  pm13.183  2911  eqeu  2943  mo2icl  2952  euind  2960  reuind  2978  cdeqal  2987  sbcal  3050  sbcalg  3051  sbcabel  3080  csbcow  3104  csbiebg  3136  ssconb  3306  reldisj  3512  sbcssg  3569  elint  3891  axsep2  4164  zfauscl  4165  bm1.3ii  4166  exmidel  4250  euotd  4300  freq1  4392  freq2  4394  eusv1  4500  ontr2exmid  4574  regexmid  4584  tfisi  4636  nnregexmid  4670  iota5  5254  sbcfung  5296  funimass4  5631  dffo3  5729  eufnfv  5817  dff13  5839  uchoice  6225  tfr1onlemsucfn  6428  tfr1onlemsucaccv  6429  tfr1onlembxssdm  6431  tfr1onlembfn  6432  tfrcllemsucfn  6441  tfrcllemsucaccv  6442  tfrcllembxssdm  6444  tfrcllembfn  6445  tfrcl  6452  frecabcl  6487  ssfiexmid  6975  domfiexmid  6977  diffitest  6986  findcard  6987  findcard2  6988  findcard2s  6989  fiintim  7030  fisseneq  7033  isomni  7240  isomnimap  7241  ismkv  7257  ismkvmap  7258  iswomni  7269  iswomnimap  7270  omniwomnimkv  7271  exmidfodomrlemr  7312  exmidfodomrlemrALT  7313  fz1sbc  10220  frecuzrdgtcl  10559  frecuzrdgfunlem  10566  zfz1iso  10988  istopg  14504  bdsep2  15859  bdsepnfALT  15862  bdzfauscl  15863  bdbm1.3ii  15864  bj-2inf  15911  bj-nn0sucALT  15951  sscoll2  15961