Theorem albidv 1838

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

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

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 1461  ax-gen 1463  ax-17 1540

This theorem depends on definitions:  df-bi 117

This theorem is referenced by:  ax11v  1841  2albidv  1881  sbal1yz  2020  eujust  2047  euf  2050  mo23  2086  axext3  2179  bm1.1  2181  eqeq1  2203  cbvabw  2319  nfceqdf  2338  ralbidv2  2499  alexeq  2890  pm13.183  2902  eqeu  2934  mo2icl  2943  euind  2951  reuind  2969  cdeqal  2978  sbcal  3041  sbcalg  3042  sbcabel  3071  csbcow  3095  csbiebg  3127  ssconb  3296  reldisj  3502  sbcssg  3559  elint  3880  axsep2  4152  zfauscl  4153  bm1.3ii  4154  exmidel  4238  euotd  4287  freq1  4379  freq2  4381  eusv1  4487  ontr2exmid  4561  regexmid  4571  tfisi  4623  nnregexmid  4657  iota5  5240  sbcfung  5282  funimass4  5611  dffo3  5709  eufnfv  5793  dff13  5815  uchoice  6195  tfr1onlemsucfn  6398  tfr1onlemsucaccv  6399  tfr1onlembxssdm  6401  tfr1onlembfn  6402  tfrcllemsucfn  6411  tfrcllemsucaccv  6412  tfrcllembxssdm  6414  tfrcllembfn  6415  tfrcl  6422  frecabcl  6457  ssfiexmid  6937  domfiexmid  6939  diffitest  6948  findcard  6949  findcard2  6950  findcard2s  6951  fiintim  6992  fisseneq  6995  isomni  7202  isomnimap  7203  ismkv  7219  ismkvmap  7220  iswomni  7231  iswomnimap  7232  omniwomnimkv  7233  exmidfodomrlemr  7269  exmidfodomrlemrALT  7270  fz1sbc  10171  frecuzrdgtcl  10504  frecuzrdgfunlem  10511  zfz1iso  10933  istopg  14235  bdsep2  15532  bdsepnfALT  15535  bdzfauscl  15536  bdbm1.3ii  15537  bj-2inf  15584  bj-nn0sucALT  15624  sscoll2  15634