Theorem albii 1447

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

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

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 1424  ax-gen 1426

This theorem depends on definitions:  df-bi 116

This theorem is referenced by:  2albii  1448  hbxfrbi  1449  nfbii  1450  19.26-2  1459  19.26-3an  1460  alrot3  1462  alrot4  1463  albiim  1464  2albiim  1465  alnex  1476  nfalt  1558  aaanh  1566  aaan  1567  alinexa  1583  exintrbi  1613  19.21-2  1646  19.31r  1660  equsalh  1705  equsal  1706  sbcof2  1783  dvelimfALT2  1790  19.23vv  1857  sbanv  1862  pm11.53  1868  nfsbxy  1916  nfsbxyt  1917  sbcomxyyz  1946  sb9  1955  sbnf2  1957  2sb6  1960  sbcom2v  1961  sb6a  1964  2sb6rf  1966  sbalyz  1975  sbal  1976  sbal1yz  1977  sbal1  1978  sbalv  1981  2exsb  1985  nfsb4t  1990  dvelimf  1991  dveeq1  1995  sbal2  1998  sb8eu  2013  sb8euh  2023  eu1  2025  eu2  2044  mo3h  2053  moanim  2074  2eu4  2093  exists1  2096  eqcom  2142  hblem  2248  abeq2  2249  abeq1  2250  nfceqi  2278  abid2f  2307  dfrex2dc  2429  ralbii2  2448  r2alf  2455  nfraldya  2472  r3al  2480  r19.21t  2510  r19.23t  2542  rabid2  2610  rabbi  2611  ralv  2706  ceqsralt  2716  gencbval  2737  rspc2gv  2805  ralab  2848  ralrab2  2853  euind  2875  reu2  2876  reu3  2878  rmo4  2881  reu8  2884  rmo3f  2885  rmoim  2889  2reuswapdc  2892  reuind  2893  2rmorex  2894  ra5  3001  rmo2ilem  3002  rmo3  3004  dfss2  3091  ss2ab  3170  ss2rab  3178  rabss  3179  uniiunlem  3190  dfdif3  3191  ddifstab  3213  ssequn1  3251  unss  3255  ralunb  3262  ssin  3303  ssddif  3315  n0rf  3380  eq0  3386  eqv  3387  rabeq0  3397  abeq0  3398  disj  3416  disj3  3420  rgenm  3470  pwss  3531  ralsnsg  3568  ralsns  3569  disjsn  3593  euabsn2  3600  snss  3657  snsssn  3696  dfnfc2  3762  uni0b  3769  unissb  3774  elintrab  3791  ssintrab  3802  intun  3810  intpr  3811  dfiin2g  3854  iunss  3862  dfdisj2  3916  cbvdisj  3924  disjnim  3928  dftr2  4036  dftr5  4037  trint  4049  zfnuleu  4060  vnex  4067  inex1  4070  repizf2lem  4093  axpweq  4103  zfpow  4107  axpow2  4108  axpow3  4109  exmid01  4129  zfpair2  4140  ssextss  4150  frirrg  4280  sucel  4340  zfun  4364  uniex2  4366  setindel  4461  setind  4462  elirr  4464  en2lp  4477  zfregfr  4496  tfi  4504  peano5  4520  ssrel  4635  ssrel2  4637  eqrelrel  4648  reliun  4668  raliunxp  4688  relop  4697  dmopab3  4760  dm0rn0  4764  reldm0  4765  cotr  4928  issref  4929  asymref  4932  intirr  4933  sb8iota  5103  dffun2  5141  dffun4  5142  dffun6f  5144  dffun4f  5147  dffun7  5158  funopab  5166  funcnv2  5191  funcnv  5192  funcnveq  5194  fun2cnv  5195  fun11  5198  fununi  5199  funcnvuni  5200  funimaexglem  5214  fnres  5247  fnopabg  5254  rexrnmpt  5571  dff13  5677  oprabidlem  5810  eqoprab2b  5837  mpo2eqb  5888  ralrnmpo  5893  dfer2  6438  fiintim  6825  omniwomnimkv  7049  ltexprlemdisj  7438  recexprlemdisj  7462  isprm2  11834  bj-stal  13128  bj-nfalt  13142  bdceq  13211  bdcriota  13252  bj-axempty2  13263  bj-vprc  13265  bdinex1  13268  bj-zfpair2  13279  bj-uniex2  13285  bj-ssom  13305  bj-inf2vnlem2  13340  ss1oel2o  13360