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

Theorem albii 1429
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 1427 . 2  |-  ( A. x ( ph  <->  ps )  ->  ( A. x ph  <->  A. x ps ) )
2 albii.1 . 2  |-  ( ph  <->  ps )
31, 2mpg 1410 1  |-  ( A. x ph  <->  A. x ps )
Colors of variables: wff set class
Syntax hints:    <-> wb 104   A.wal 1312
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 1406  ax-gen 1408
This theorem depends on definitions:  df-bi 116
This theorem is referenced by:  2albii  1430  hbxfrbi  1431  nfbii  1432  19.26-2  1441  19.26-3an  1442  alrot3  1444  alrot4  1445  albiim  1446  2albiim  1447  alnex  1458  nfalt  1540  aaanh  1548  aaan  1549  alinexa  1565  exintrbi  1595  19.21-2  1628  19.31r  1642  equsalh  1687  equsal  1688  sbcof2  1764  dvelimfALT2  1771  19.23vv  1838  sbanv  1843  pm11.53  1849  nfsbxy  1893  nfsbxyt  1894  sbcomxyyz  1921  sb9  1930  sbnf2  1932  2sb6  1935  sbcom2v  1936  sb6a  1939  2sb6rf  1941  sbalyz  1950  sbal  1951  sbal1yz  1952  sbal1  1953  sbalv  1956  2exsb  1960  nfsb4t  1965  dvelimf  1966  dveeq1  1970  sbal2  1973  sb8eu  1988  sb8euh  1998  eu1  2000  eu2  2019  mo3h  2028  moanim  2049  2eu4  2068  exists1  2071  eqcom  2117  hblem  2223  abeq2  2224  abeq1  2225  nfceqi  2252  abid2f  2281  dfrex2dc  2403  ralbii2  2420  r2alf  2427  nfraldya  2444  r3al  2452  r19.21t  2482  r19.23t  2514  rabid2  2582  rabbi  2583  ralv  2675  ceqsralt  2685  gencbval  2706  rspc2gv  2773  ralab  2815  ralrab2  2820  euind  2842  reu2  2843  reu3  2845  rmo4  2848  reu8  2851  rmo3f  2852  rmoim  2856  2reuswapdc  2859  reuind  2860  2rmorex  2861  ra5  2967  rmo2ilem  2968  rmo3  2970  dfss2  3054  ss2ab  3133  ss2rab  3141  rabss  3142  uniiunlem  3153  dfdif3  3154  ddifstab  3176  ssequn1  3214  unss  3218  ralunb  3225  ssin  3266  ssddif  3278  n0rf  3343  eq0  3349  eqv  3350  rabeq0  3360  abeq0  3361  disj  3379  disj3  3383  rgenm  3433  pwss  3494  ralsnsg  3529  ralsns  3530  disjsn  3553  euabsn2  3560  snss  3617  snsssn  3656  dfnfc2  3722  uni0b  3729  unissb  3734  elintrab  3751  ssintrab  3762  intun  3770  intpr  3771  dfiin2g  3814  iunss  3822  dfdisj2  3876  cbvdisj  3884  disjnim  3888  dftr2  3996  dftr5  3997  trint  4009  zfnuleu  4020  vnex  4027  inex1  4030  repizf2lem  4053  axpweq  4063  zfpow  4067  axpow2  4068  axpow3  4069  exmid01  4089  zfpair2  4100  ssextss  4110  frirrg  4240  sucel  4300  zfun  4324  uniex2  4326  setindel  4421  setind  4422  elirr  4424  en2lp  4437  zfregfr  4456  tfi  4464  peano5  4480  ssrel  4595  ssrel2  4597  eqrelrel  4608  reliun  4628  raliunxp  4648  relop  4657  dmopab3  4720  dm0rn0  4724  reldm0  4725  cotr  4888  issref  4889  asymref  4892  intirr  4893  sb8iota  5063  dffun2  5101  dffun4  5102  dffun6f  5104  dffun4f  5107  dffun7  5118  funopab  5126  funcnv2  5151  funcnv  5152  funcnveq  5154  fun2cnv  5155  fun11  5158  fununi  5159  funcnvuni  5160  funimaexglem  5174  fnres  5207  fnopabg  5214  rexrnmpt  5529  dff13  5635  oprabidlem  5768  eqoprab2b  5795  mpo2eqb  5846  ralrnmpo  5851  dfer2  6396  fiintim  6783  ltexprlemdisj  7378  recexprlemdisj  7402  isprm2  11694  bj-stal  12768  bj-nfalt  12782  bdceq  12851  bdcriota  12892  bj-axempty2  12903  bj-vprc  12905  bdinex1  12908  bj-zfpair2  12919  bj-uniex2  12925  bj-ssom  12945  bj-inf2vnlem2  12980  ss1oel2o  13000
  Copyright terms: Public domain W3C validator