Theorem albii 1405

Description: Inference adding universal quantifier to both sides of an equivalence. (Contributed by NM, 7-Aug-1994.)

Hypothesis

Ref	Expression
albii.1	|- ( ph <-> ps )

Assertion

Ref	Expression
albii	|- ( A. x ph <-> A. x ps )

Proof of Theorem albii

Step	Hyp	Ref	Expression
1		albi 1403	. 2 |- ( A. x ( ph <-> ps ) -> ( A. x ph <-> A. x ps ) )
2		albii.1	. 2 |- ( ph <-> ps )
3	1, 2	mpg 1386	1 |- ( A. x ph <-> A. x ps )

Syntax hints:   <-> wb 104   A.wal 1288

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 1382  ax-gen 1384

This theorem depends on definitions:  df-bi 116

This theorem is referenced by:  2albii  1406  hbxfrbi  1407  nfbii  1408  19.26-2  1417  19.26-3an  1418  alrot3  1420  alrot4  1421  albiim  1422  2albiim  1423  alnex  1434  nfalt  1516  aaanh  1524  aaan  1525  alinexa  1540  exintrbi  1570  19.21-2  1603  19.31r  1617  equsalh  1662  equsal  1663  sbcof2  1739  dvelimfALT2  1746  19.23vv  1813  sbanv  1818  pm11.53  1824  nfsbxy  1867  nfsbxyt  1868  sbcomxyyz  1895  sb9  1904  sbnf2  1906  2sb6  1909  sbcom2v  1910  sb6a  1913  2sb6rf  1915  sbalyz  1924  sbal  1925  sbal1yz  1926  sbal1  1927  sbalv  1930  2exsb  1934  nfsb4t  1939  dvelimf  1940  dveeq1  1944  sbal2  1947  sb8eu  1962  sb8euh  1972  eu1  1974  eu2  1993  mo3h  2002  moanim  2023  2eu4  2042  exists1  2045  eqcom  2091  hblem  2196  abeq2  2197  abeq1  2198  nfceqi  2225  abid2f  2254  dfrex2dc  2372  ralbii2  2389  r2alf  2396  nfraldya  2413  r3al  2421  r19.21t  2449  r19.23t  2481  rabid2  2546  rabbi  2547  ralv  2639  ceqsralt  2649  gencbval  2670  rspc2gv  2736  ralab  2778  ralrab2  2783  euind  2805  reu2  2806  reu3  2808  rmo4  2811  reu8  2814  rmo3f  2815  rmoim  2819  2reuswapdc  2822  reuind  2823  2rmorex  2824  ra5  2930  rmo2ilem  2931  rmo3  2933  dfss2  3017  ss2ab  3092  ss2rab  3100  rabss  3101  uniiunlem  3112  dfdif3  3113  ddifstab  3135  ssequn1  3173  unss  3177  ralunb  3184  ssin  3225  ssddif  3236  n0rf  3301  eq0  3307  eqv  3308  rabeq0  3318  abeq0  3319  disj  3337  disj3  3341  rgenm  3390  pwss  3451  ralsnsg  3486  ralsns  3487  disjsn  3510  euabsn2  3517  snss  3574  snsssn  3613  dfnfc2  3679  uni0b  3686  unissb  3691  elintrab  3708  ssintrab  3719  intun  3727  intpr  3728  dfiin2g  3771  iunss  3779  dfdisj2  3832  cbvdisj  3840  disjnim  3844  dftr2  3946  dftr5  3947  trint  3959  zfnuleu  3971  vnex  3978  inex1  3981  repizf2lem  4004  axpweq  4014  zfpow  4018  axpow2  4019  axpow3  4020  exmid01  4040  zfpair2  4048  ssextss  4058  frirrg  4188  sucel  4248  zfun  4272  uniex2  4274  setindel  4369  setind  4370  elirr  4372  en2lp  4385  zfregfr  4404  tfi  4412  peano5  4428  ssrel  4541  ssrel2  4543  eqrelrel  4554  reliun  4573  raliunxp  4592  relop  4601  dmopab3  4664  dm0rn0  4668  reldm0  4669  cotr  4828  issref  4829  asymref  4832  intirr  4833  sb8iota  5002  dffun2  5040  dffun4  5041  dffun6f  5043  dffun4f  5046  dffun7  5057  funopab  5064  funcnv2  5089  funcnv  5090  funcnveq  5092  fun2cnv  5093  fun11  5096  fununi  5097  funcnvuni  5098  funimaexglem  5112  fnres  5145  fnopabg  5152  rexrnmpt  5458  dff13  5563  oprabidlem  5696  eqoprab2b  5723  mpt22eqb  5770  ralrnmpt2  5775  dfer2  6309  fiintim  6695  ltexprlemdisj  7228  recexprlemdisj  7252  isprm2  11440  bj-nfalt  11969  bdceq  12037  bdcriota  12078  bj-axempty2  12089  bj-vprc  12091  bdinex1  12094  bj-zfpair2  12105  bj-uniex2  12111  bj-ssom  12135  bj-inf2vnlem2  12170  ss1oel2o  12192