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  2057  eujust  2084  euf  2087  mo23  2124  axext3  2217  bm1.1  2219  eqeq1  2241  cbvabw  2359  nfceqdf  2385  ralbidv2  2546  alexeq  2946  pm13.183  2958  eqeu  2990  mo2icl  2999  euind  3007  reuind  3025  cdeqal  3034  sbcal  3097  sbcalg  3098  sbcabel  3128  csbcow  3152  csbiebg  3184  ssconb  3356  reldisj  3564  sbcssg  3622  elint  3960  axsep2  4234  zfauscl  4235  bm1.3ii  4236  exmidel  4323  euotd  4376  freq1  4470  freq2  4472  eusv1  4578  ontr2exmid  4652  regexmid  4662  tfisi  4714  nnregexmid  4748  iota5  5339  sbcfung  5381  funimass4  5732  dffo3  5829  eufnfv  5922  dff13  5947  uchoice  6344  tfr1onlemsucfn  6584  tfr1onlemsucaccv  6585  tfr1onlembxssdm  6587  tfr1onlembfn  6588  tfrcllemsucfn  6597  tfrcllemsucaccv  6598  tfrcllembxssdm  6600  tfrcllembfn  6601  tfrcl  6608  frecabcl  6643  modom  7074  ssfiexmid  7144  ssfiexmidt  7146  domfiexmid  7148  diffitest  7157  findcard  7158  findcard2  7159  findcard2s  7160  fiintim  7204  fisseneq  7208  isomni  7440  isomnimap  7441  ismkv  7457  ismkvmap  7458  iswomni  7469  iswomnimap  7470  omniwomnimkv  7471  exmidfodomrlemr  7518  exmidfodomrlemrALT  7519  fz1sbc  10452  frecuzrdgtcl  10798  frecuzrdgfunlem  10805  zfz1iso  11238  istopg  14990  bdsep2  16782  bdsepnfALT  16785  bdzfauscl  16786  bdbm1.3ii  16787  bj-2inf  16834  bj-nn0sucALT  16874  sscoll2  16884