Theorem albii 1446

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 1444	. 2 |- ( A. x ( ph <-> ps ) -> ( A. x ph <-> A. x ps ) )
2		albii.1	. 2 |- ( ph <-> ps )
3	1, 2	mpg 1427	1 |- ( A. x ph <-> A. x ps )

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

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-5 1423  ax-gen 1425

This theorem depends on definitions:  df-bi 116

This theorem is referenced by:  2albii  1447  hbxfrbi  1448  nfbii  1449  19.26-2  1458  19.26-3an  1459  alrot3  1461  alrot4  1462  albiim  1463  2albiim  1464  alnex  1475  nfalt  1557  aaanh  1565  aaan  1566  alinexa  1582  exintrbi  1612  19.21-2  1645  19.31r  1659  equsalh  1704  equsal  1705  sbcof2  1782  dvelimfALT2  1789  19.23vv  1856  sbanv  1861  pm11.53  1867  nfsbxy  1915  nfsbxyt  1916  sbcomxyyz  1945  sb9  1954  sbnf2  1956  2sb6  1959  sbcom2v  1960  sb6a  1963  2sb6rf  1965  sbalyz  1974  sbal  1975  sbal1yz  1976  sbal1  1977  sbalv  1980  2exsb  1984  nfsb4t  1989  dvelimf  1990  dveeq1  1994  sbal2  1997  sb8eu  2012  sb8euh  2022  eu1  2024  eu2  2043  mo3h  2052  moanim  2073  2eu4  2092  exists1  2095  eqcom  2141  hblem  2247  abeq2  2248  abeq1  2249  nfceqi  2277  abid2f  2306  dfrex2dc  2428  ralbii2  2445  r2alf  2452  nfraldya  2469  r3al  2477  r19.21t  2507  r19.23t  2539  rabid2  2607  rabbi  2608  ralv  2703  ceqsralt  2713  gencbval  2734  rspc2gv  2801  ralab  2844  ralrab2  2849  euind  2871  reu2  2872  reu3  2874  rmo4  2877  reu8  2880  rmo3f  2881  rmoim  2885  2reuswapdc  2888  reuind  2889  2rmorex  2890  ra5  2997  rmo2ilem  2998  rmo3  3000  dfss2  3086  ss2ab  3165  ss2rab  3173  rabss  3174  uniiunlem  3185  dfdif3  3186  ddifstab  3208  ssequn1  3246  unss  3250  ralunb  3257  ssin  3298  ssddif  3310  n0rf  3375  eq0  3381  eqv  3382  rabeq0  3392  abeq0  3393  disj  3411  disj3  3415  rgenm  3465  pwss  3526  ralsnsg  3561  ralsns  3562  disjsn  3585  euabsn2  3592  snss  3649  snsssn  3688  dfnfc2  3754  uni0b  3761  unissb  3766  elintrab  3783  ssintrab  3794  intun  3802  intpr  3803  dfiin2g  3846  iunss  3854  dfdisj2  3908  cbvdisj  3916  disjnim  3920  dftr2  4028  dftr5  4029  trint  4041  zfnuleu  4052  vnex  4059  inex1  4062  repizf2lem  4085  axpweq  4095  zfpow  4099  axpow2  4100  axpow3  4101  exmid01  4121  zfpair2  4132  ssextss  4142  frirrg  4272  sucel  4332  zfun  4356  uniex2  4358  setindel  4453  setind  4454  elirr  4456  en2lp  4469  zfregfr  4488  tfi  4496  peano5  4512  ssrel  4627  ssrel2  4629  eqrelrel  4640  reliun  4660  raliunxp  4680  relop  4689  dmopab3  4752  dm0rn0  4756  reldm0  4757  cotr  4920  issref  4921  asymref  4924  intirr  4925  sb8iota  5095  dffun2  5133  dffun4  5134  dffun6f  5136  dffun4f  5139  dffun7  5150  funopab  5158  funcnv2  5183  funcnv  5184  funcnveq  5186  fun2cnv  5187  fun11  5190  fununi  5191  funcnvuni  5192  funimaexglem  5206  fnres  5239  fnopabg  5246  rexrnmpt  5563  dff13  5669  oprabidlem  5802  eqoprab2b  5829  mpo2eqb  5880  ralrnmpo  5885  dfer2  6430  fiintim  6817  ltexprlemdisj  7414  recexprlemdisj  7438  isprm2  11798  bj-stal  12957  bj-nfalt  12971  bdceq  13040  bdcriota  13081  bj-axempty2  13092  bj-vprc  13094  bdinex1  13097  bj-zfpair2  13108  bj-uniex2  13114  bj-ssom  13134  bj-inf2vnlem2  13169  ss1oel2o  13189