Theorem albidv 1804

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

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

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 1427  ax-gen 1429  ax-17 1506

This theorem depends on definitions:  df-bi 116

This theorem is referenced by:  ax11v  1807  2albidv  1847  sbal1yz  1981  eujust  2008  euf  2011  mo23  2047  axext3  2140  bm1.1  2142  eqeq1  2164  cbvabw  2280  nfceqdf  2298  ralbidv2  2459  alexeq  2838  pm13.183  2850  eqeu  2882  mo2icl  2891  euind  2899  reuind  2917  cdeqal  2926  sbcal  2988  sbcalg  2989  sbcabel  3018  csbcow  3042  csbiebg  3073  ssconb  3240  reldisj  3445  sbcssg  3503  elint  3813  axsep2  4083  zfauscl  4084  bm1.3ii  4085  exmidel  4166  euotd  4214  freq1  4304  freq2  4306  eusv1  4412  ontr2exmid  4484  regexmid  4494  tfisi  4546  nnregexmid  4580  iota5  5155  sbcfung  5194  funimass4  5519  dffo3  5614  eufnfv  5697  dff13  5718  tfr1onlemsucfn  6287  tfr1onlemsucaccv  6288  tfr1onlembxssdm  6290  tfr1onlembfn  6291  tfrcllemsucfn  6300  tfrcllemsucaccv  6301  tfrcllembxssdm  6303  tfrcllembfn  6304  tfrcl  6311  frecabcl  6346  ssfiexmid  6821  domfiexmid  6823  diffitest  6832  findcard  6833  findcard2  6834  findcard2s  6835  fiintim  6873  fisseneq  6876  isomni  7079  isomnimap  7080  ismkv  7096  ismkvmap  7097  iswomni  7108  iswomnimap  7109  omniwomnimkv  7110  exmidfodomrlemr  7137  exmidfodomrlemrALT  7138  fz1sbc  9998  frecuzrdgtcl  10311  frecuzrdgfunlem  10318  zfz1iso  10712  istopg  12397  bdsep2  13461  bdsepnfALT  13464  bdzfauscl  13465  bdbm1.3ii  13466  bj-2inf  13513  bj-nn0sucALT  13553  sscoll2  13563