Theorem albii 1566

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

Hypothesis

Ref	Expression
albii.1	⊢ (φ ↔ ψ)

Assertion

Ref	Expression
albii	⊢ (∀xφ ↔ ∀xψ)

Proof of Theorem albii

Step	Hyp	Ref	Expression
1		albi 1564	. 2 ⊢ (∀x(φ ↔ ψ) → (∀xφ ↔ ∀xψ))
2		albii.1	. 2 ⊢ (φ ↔ ψ)
3	1, 2	mpg 1548	1 ⊢ (∀xφ ↔ ∀xψ)

Syntax hints:   ↔ wb 176  ∀wal 1540

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1546  ax-5 1557

This theorem depends on definitions:  df-bi 177

This theorem is referenced by:  2albii  1567  hbxfrbi  1568  nfbii  1569  alex  1572  2nalexn  1573  alinexa  1578  alexn  1579  19.26-2  1594  19.26-3an  1595  19.35  1600  19.30  1604  19.43OLD  1606  albiim  1611  2albiim  1612  exintrbi  1613  19.8wOLD  1693  alrot3  1738  alrot4  1739  hba1  1786  equsalhw  1838  equsalhwOLD  1839  dvelimhw  1849  19.21-2  1864  19.32  1875  19.31  1876  aaan  1884  19.23vv  1892  pm11.53  1893  19.12vv  1898  ax12olem2  1928  equsal  1960  dvelimh  1964  sbcom  2089  sb8e  2093  sbnf2  2108  2sb6  2113  sbcom2  2114  sb6a  2116  2sb6rf  2118  sbex  2128  sbalv  2129  2exsb  2132  dvelimALT  2133  sbal2  2134  dvelimf-o  2180  ax10-16  2190  sb8eu  2222  eu1  2225  eu2  2229  moanim  2260  2mo  2282  2eu3  2286  2eu4  2287  exists1  2293  eqcom  2355  hblem  2457  abeq2  2458  abeq1  2459  nfceqi  2485  abid2f  2514  ralbii2  2642  r2alf  2649  r3al  2671  r19.21t  2699  r19.23t  2728  rabid2  2788  rabbi  2789  ralv  2872  ceqsralt  2882  ralab  2997  ralrab2  3002  euind  3023  reu2  3024  reu3  3026  rmo4  3029  reu8  3032  rmoim  3035  2reuswap  3038  reuind  3039  2reu5lem2  3042  2reu5lem3  3043  ra5  3130  rmo2  3131  rmo3  3133  dfss2  3262  ss2ab  3334  ss2rab  3342  rabss  3343  uniiunlem  3353  ssequn1  3433  unss  3437  ralunb  3444  ssin  3477  n0f  3558  eqv  3565  disj  3591  disj3  3595  ssdif0  3609  inssdif0  3617  ssundif  3633  sscon34  3661  pwss  3736  ralsns  3763  disjsn  3786  euabsn2  3791  snss  3838  pwpw0  3855  pwsnALT  3882  dfnfc2  3909  unissb  3921  elintrab  3938  ssintrab  3949  intun  3958  intpr  3959  dfiin2g  4000  iunss  4007  axprimlem1  4088  axprimlem2  4089  axxpprim  4090  axsiprim  4093  axtyplowerprim  4094  axins2prim  4095  axins3prim  4096  ninexg  4097  1cex  4142  eqpw1  4162  pw111  4170  ssrelk  4211  eqrelk  4212  elp6  4263  xpkvexg  4285  p6exg  4290  dfuni12  4291  sikexlem  4295  dfimak2  4298  insklem  4304  ins2kexg  4305  ins3kexg  4306  sb8iota  4346  ssfin  4470  nnadjoin  4520  nnadjoinpw  4521  nnpweq  4523  tfinnn  4534  spfininduct  4540  eqop  4611  raliunxp  4823  ssopr  4846  eqopr  4847  dmopab3  4917  dm0rn0  4921  dmeq0  4922  cotr  5026  intirr  5029  dffun3  5120  dffun4  5121  dffun5  5122  dffun6f  5123  dffun7  5133  funopab  5139  funcnv2  5155  funcnv  5156  fun11  5159  fununi  5160  funcnvuni  5161  fnres  5199  fnopabg  5205  dff13  5471  fvfullfunlem1  5861  clos1induct  5880  dfnnc3  5885  frds  5935  enmap2lem4  6066  enmap1lem4  6072  ncssfin  6151  spacind  6287