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  7477  isomnimap  7478  ismkv  7494  ismkvmap  7495  iswomni  7506  iswomnimap  7507  omniwomnimkv  7508  exmidfodomrlemr  7555  exmidfodomrlemrALT  7556  fz1sbc  10514  frecuzrdgtcl  10864  frecuzrdgfunlem  10871  zfz1iso  11309  istopg  15191  bdsep2  17078  bdsepnfALT  17081  bdsepg  17082  bdbm1.3ii  17083  bj-2inf  17130  bj-nn0sucALT  17170  sscoll2  17180  wexmiddiffilem  17209  wexmiddifxy  17212