Theorem albidv 1873

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

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

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 1496  ax-gen 1498  ax-17 1575

This theorem depends on definitions:  df-bi 117

This theorem is referenced by:  ax11v  1876  2albidv  1916  sbal1yz  2055  eujust  2082  euf  2085  mo23  2122  axext3  2215  bm1.1  2217  eqeq1  2239  cbvabw  2357  nfceqdf  2383  ralbidv2  2544  alexeq  2943  pm13.183  2955  eqeu  2987  mo2icl  2996  euind  3004  reuind  3022  cdeqal  3031  sbcal  3094  sbcalg  3095  sbcabel  3125  csbcow  3149  csbiebg  3181  ssconb  3352  reldisj  3560  sbcssg  3618  elint  3955  axsep2  4229  zfauscl  4230  bm1.3ii  4231  exmidel  4318  euotd  4371  freq1  4465  freq2  4467  eusv1  4573  ontr2exmid  4647  regexmid  4657  tfisi  4709  nnregexmid  4743  iota5  5334  sbcfung  5376  funimass4  5727  dffo3  5824  eufnfv  5917  dff13  5941  uchoice  6331  tfr1onlemsucfn  6571  tfr1onlemsucaccv  6572  tfr1onlembxssdm  6574  tfr1onlembfn  6575  tfrcllemsucfn  6584  tfrcllemsucaccv  6585  tfrcllembxssdm  6587  tfrcllembfn  6588  tfrcl  6595  frecabcl  6630  modom  7061  ssfiexmid  7131  ssfiexmidt  7133  domfiexmid  7135  diffitest  7144  findcard  7145  findcard2  7146  findcard2s  7147  fiintim  7191  fisseneq  7195  isomni  7427  isomnimap  7428  ismkv  7444  ismkvmap  7445  iswomni  7456  iswomnimap  7457  omniwomnimkv  7458  exmidfodomrlemr  7505  exmidfodomrlemrALT  7506  fz1sbc  10430  frecuzrdgtcl  10774  frecuzrdgfunlem  10781  zfz1iso  11213  istopg  14864  bdsep2  16656  bdsepnfALT  16659  bdzfauscl  16660  bdbm1.3ii  16661  bj-2inf  16708  bj-nn0sucALT  16748  sscoll2  16758