Theorem albidv 1759

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

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

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-5 1388  ax-gen 1390  ax-17 1471

This theorem depends on definitions:  df-bi 116

This theorem is referenced by:  ax11v  1762  2albidv  1802  sbal1yz  1932  eujust  1957  euf  1960  mo23  1996  axext3  2078  bm1.1  2080  eqeq1  2101  nfceqdf  2234  ralbidv2  2393  alexeq  2757  pm13.183  2768  eqeu  2799  mo2icl  2808  euind  2816  reuind  2834  cdeqal  2843  sbcal  2904  sbcalg  2905  sbcabel  2934  csbiebg  2984  ssconb  3148  reldisj  3353  sbcssg  3411  elint  3716  axsep2  3979  zfauscl  3980  bm1.3ii  3981  exmidel  4057  euotd  4105  freq1  4195  freq2  4197  eusv1  4302  ontr2exmid  4369  regexmid  4379  tfisi  4430  nnregexmid  4462  iota5  5034  sbcfung  5073  funimass4  5390  dffo3  5485  eufnfv  5564  dff13  5585  tfr1onlemsucfn  6143  tfr1onlemsucaccv  6144  tfr1onlembxssdm  6146  tfr1onlembfn  6147  tfrcllemsucfn  6156  tfrcllemsucaccv  6157  tfrcllembxssdm  6159  tfrcllembfn  6160  tfrcl  6167  frecabcl  6202  ssfiexmid  6672  domfiexmid  6674  diffitest  6683  findcard  6684  findcard2  6685  findcard2s  6686  fiintim  6719  fisseneq  6722  isomni  6879  isomnimap  6880  ismkv  6897  ismkvmap  6898  exmidfodomrlemr  6925  exmidfodomrlemrALT  6926  fz1sbc  9659  frecuzrdgtcl  9968  frecuzrdgfunlem  9975  zfz1iso  10361  istopg  11850  bdsep2  12485  bdsepnfALT  12488  bdzfauscl  12489  bdbm1.3ii  12490  bj-2inf  12541  bj-nn0sucALT  12581  strcoll2  12586  strcollnfALT  12589