Theorem albidv 1877

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

This proof depends on syntax axioms:   -> wi 4   <-> wb 105   A.wal 1400

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-5 1500  ax-gen 1502  ax-17 1579

This proof depends on definitions:  df-bi 117

This theorem is used by:  ax11v  1880  2albidv  1920  sbal1yz  2061  eujust  2088  euf  2091  mo23  2128  axext3  2221  bm1.1  2223  eqeq1  2245  cbvabw  2363  nfceqdf  2391  ralbidv2  2552  alexeq  2952  pm13.183  2964  eqeu  2996  mo2icl  3005  euind  3013  reuind  3031  cdeqal  3040  sbcal  3103  sbcalg  3104  sbcabel  3134  csbcow  3158  csbiebg  3190  ssconb  3362  reldisj  3576  sbcssg  3636  elint  3976  axsepg  4250  sepg  4251  zfausclOLD  4253  bm1.3ii  4254  exmidel  4342  euotd  4395  freq1  4489  freq2  4491  eusv1  4598  ontr2exmid  4672  regexmid  4682  tfisi  4734  nnregexmid  4768  iota5  5359  sbcfung  5401  funimass4  5753  dffo3  5855  eufnfv  5949  dff13  5974  uchoice  6371  tfr1onlemsucfn  6611  tfr1onlemsucaccv  6612  tfr1onlembxssdm  6614  tfr1onlembfn  6615  tfrcllemsucfn  6624  tfrcllemsucaccv  6625  tfrcllembxssdm  6627  tfrcllembfn  6628  tfrcl  6635  frecabcl  6670  modom  7108  ssfiexmid  7178  ssfiexmidt  7180  domfiexmid  7182  diffitest  7191  findcard  7192  findcard2  7193  findcard2s  7194  fiintim  7238  fisseneq  7242  isomni  7476  isomnimap  7477  ismkv  7493  ismkvmap  7494  iswomni  7505  iswomnimap  7506  omniwomnimkv  7507  exmidfodomrlemr  7554  exmidfodomrlemrALT  7555  fz1sbc  10503  frecuzrdgtcl  10849  frecuzrdgfunlem  10856  zfz1iso  11293  istopg  15100  bdsep2  16912  bdsepnfALT  16915  bdsepg  16916  bdbm1.3ii  16917  bj-2inf  16964  bj-nn0sucALT  17004  sscoll2  17014  wexmiddiffilem  17043  wexmiddifxy  17046