ILE Home Intuitionistic Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  ILE Home  >  Th. List  >  albii Unicode version

Theorem albii 1375
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
StepHypRef Expression
1 albi 1373 . 2  |-  ( A. x ( ph  <->  ps )  ->  ( A. x ph  <->  A. x ps ) )
2 albii.1 . 2  |-  ( ph  <->  ps )
31, 2mpg 1356 1  |-  ( A. x ph  <->  A. x ps )
Colors of variables: wff set class
Syntax hints:    <-> wb 102   A.wal 1257
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 103  ax-ia2 104  ax-ia3 105  ax-5 1352  ax-gen 1354
This theorem depends on definitions:  df-bi 114
This theorem is referenced by:  2albii  1376  hbxfrbi  1377  nfbii  1378  19.26-2  1387  19.26-3an  1388  alrot3  1390  alrot4  1391  albiim  1392  2albiim  1393  alnex  1404  nfalt  1486  aaanh  1494  aaan  1495  alinexa  1510  exintrbi  1540  19.21-2  1573  19.31r  1587  equsalh  1630  equsal  1631  sbcof2  1707  dvelimfALT2  1714  19.23vv  1780  sbanv  1785  pm11.53  1791  nfsbxy  1834  nfsbxyt  1835  sbcomxyyz  1862  sb9  1871  sbnf2  1873  2sb6  1876  sbcom2v  1877  sb6a  1880  2sb6rf  1882  sbalyz  1891  sbal  1892  sbal1yz  1893  sbal1  1894  sbalv  1897  2exsb  1901  nfsb4t  1906  dvelimf  1907  dveeq1  1911  sbal2  1914  sb8eu  1929  sb8euh  1939  eu1  1941  eu2  1960  mo3h  1969  moanim  1990  2eu4  2009  exists1  2012  eqcom  2058  hblem  2161  abeq2  2162  abeq1  2163  nfceqi  2190  abid2f  2218  ralbii2  2351  r2alf  2358  nfraldya  2375  r3al  2383  r19.21t  2411  r19.23t  2440  rabid2  2503  rabbi  2504  ralv  2588  ceqsralt  2598  gencbval  2619  rspc2gv  2684  ralab  2724  ralrab2  2729  euind  2751  reu2  2752  reu3  2754  rmo4  2757  reu8  2760  rmoim  2763  2reuswapdc  2766  reuind  2767  2rmorex  2768  ra5  2874  rmo2ilem  2875  rmo3  2877  dfss2  2962  ss2ab  3036  ss2rab  3044  rabss  3045  uniiunlem  3056  ssequn1  3141  unss  3145  ralunb  3152  ssin  3187  ssddif  3199  n0rf  3261  eq0  3267  eqv  3268  rabeq0  3275  abeq0  3276  disj  3296  disj3  3300  rgenm  3351  pwss  3402  ralsnsg  3435  ralsns  3436  disjsn  3460  euabsn2  3467  snss  3522  snsssn  3560  dfnfc2  3626  uni0b  3633  unissb  3638  elintrab  3655  ssintrab  3666  intun  3674  intpr  3675  dfiin2g  3718  iunss  3726  dfdisj2  3775  cbvdisj  3783  dftr2  3884  dftr5  3885  trint  3897  zfnuleu  3909  vprc  3916  inex1  3919  repizf2lem  3942  axpweq  3952  zfpow  3956  axpow2  3957  axpow3  3958  zfpair2  3973  ssextss  3984  frirrg  4115  sucel  4175  zfun  4199  uniex2  4201  setindel  4291  setind  4292  elirr  4294  en2lp  4306  zfregfr  4326  tfi  4333  peano5  4349  ssrel  4456  ssrel2  4458  eqrelrel  4469  reliun  4486  raliunxp  4505  relop  4514  dmopab3  4576  dm0rn0  4580  reldm0  4581  cotr  4734  issref  4735  asymref  4738  intirr  4739  sb8iota  4902  dffun2  4940  dffun4  4941  dffun6f  4943  dffun4f  4946  dffun7  4956  funopab  4963  funcnv2  4987  funcnv  4988  funcnveq  4990  fun2cnv  4991  fun11  4994  fununi  4995  funcnvuni  4996  funimaexglem  5010  fnres  5043  fnopabg  5050  rexrnmpt  5338  dff13  5435  oprabidlem  5564  eqoprab2b  5591  mpt22eqb  5638  ralrnmpt2  5643  dfer2  6138  ltexprlemdisj  6762  recexprlemdisj  6786  bj-nfalt  10291  bdceq  10349  bdcriota  10390  bj-axempty2  10401  bj-vprc  10403  bdinex1  10406  bj-zfpair2  10417  bj-uniex2  10423  bj-ssom  10447  peano5setOLD  10452  bj-inf2vnlem2  10483
  Copyright terms: Public domain W3C validator