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  1913  nfsbxyt  1914  sbcomxyyz  1943  sb9  1952  sbnf2  1954  2sb6  1957  sbcom2v  1958  sb6a  1961  2sb6rf  1963  sbalyz  1972  sbal  1973  sbal1yz  1974  sbal1  1975  sbalv  1978  2exsb  1982  nfsb4t  1987  dvelimf  1988  dveeq1  1992  sbal2  1995  sb8eu  2010  sb8euh  2020  eu1  2022  eu2  2041  mo3h  2050  moanim  2071  2eu4  2090  exists1  2093  eqcom  2139  hblem  2245  abeq2  2246  abeq1  2247  nfceqi  2275  abid2f  2304  dfrex2dc  2426  ralbii2  2443  r2alf  2450  nfraldya  2467  r3al  2475  r19.21t  2505  r19.23t  2537  rabid2  2605  rabbi  2606  ralv  2698  ceqsralt  2708  gencbval  2729  rspc2gv  2796  ralab  2839  ralrab2  2844  euind  2866  reu2  2867  reu3  2869  rmo4  2872  reu8  2875  rmo3f  2876  rmoim  2880  2reuswapdc  2883  reuind  2884  2rmorex  2885  ra5  2992  rmo2ilem  2993  rmo3  2995  dfss2  3081  ss2ab  3160  ss2rab  3168  rabss  3169  uniiunlem  3180  dfdif3  3181  ddifstab  3203  ssequn1  3241  unss  3245  ralunb  3252  ssin  3293  ssddif  3305  n0rf  3370  eq0  3376  eqv  3377  rabeq0  3387  abeq0  3388  disj  3406  disj3  3410  rgenm  3460  pwss  3521  ralsnsg  3556  ralsns  3557  disjsn  3580  euabsn2  3587  snss  3644  snsssn  3683  dfnfc2  3749  uni0b  3756  unissb  3761  elintrab  3778  ssintrab  3789  intun  3797  intpr  3798  dfiin2g  3841  iunss  3849  dfdisj2  3903  cbvdisj  3911  disjnim  3915  dftr2  4023  dftr5  4024  trint  4036  zfnuleu  4047  vnex  4054  inex1  4057  repizf2lem  4080  axpweq  4090  zfpow  4094  axpow2  4095  axpow3  4096  exmid01  4116  zfpair2  4127  ssextss  4137  frirrg  4267  sucel  4327  zfun  4351  uniex2  4353  setindel  4448  setind  4449  elirr  4451  en2lp  4464  zfregfr  4483  tfi  4491  peano5  4507  ssrel  4622  ssrel2  4624  eqrelrel  4635  reliun  4655  raliunxp  4675  relop  4684  dmopab3  4747  dm0rn0  4751  reldm0  4752  cotr  4915  issref  4916  asymref  4919  intirr  4920  sb8iota  5090  dffun2  5128  dffun4  5129  dffun6f  5131  dffun4f  5134  dffun7  5145  funopab  5153  funcnv2  5178  funcnv  5179  funcnveq  5181  fun2cnv  5182  fun11  5185  fununi  5186  funcnvuni  5187  funimaexglem  5201  fnres  5234  fnopabg  5241  rexrnmpt  5556  dff13  5662  oprabidlem  5795  eqoprab2b  5822  mpo2eqb  5873  ralrnmpo  5878  dfer2  6423  fiintim  6810  ltexprlemdisj  7407  recexprlemdisj  7431  isprm2  11787  bj-stal  12946  bj-nfalt  12960  bdceq  13029  bdcriota  13070  bj-axempty2  13081  bj-vprc  13083  bdinex1  13086  bj-zfpair2  13097  bj-uniex2  13103  bj-ssom  13123  bj-inf2vnlem2  13158  ss1oel2o  13178