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

Theorem albii 1402
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 1400 . 2  |-  ( A. x ( ph  <->  ps )  ->  ( A. x ph  <->  A. x ps ) )
2 albii.1 . 2  |-  ( ph  <->  ps )
31, 2mpg 1383 1  |-  ( A. x ph  <->  A. x ps )
Colors of variables: wff set class
Syntax hints:    <-> wb 103   A.wal 1285
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 104  ax-ia2 105  ax-ia3 106  ax-5 1379  ax-gen 1381
This theorem depends on definitions:  df-bi 115
This theorem is referenced by:  2albii  1403  hbxfrbi  1404  nfbii  1405  19.26-2  1414  19.26-3an  1415  alrot3  1417  alrot4  1418  albiim  1419  2albiim  1420  alnex  1431  nfalt  1513  aaanh  1521  aaan  1522  alinexa  1537  exintrbi  1567  19.21-2  1600  19.31r  1614  equsalh  1658  equsal  1659  sbcof2  1735  dvelimfALT2  1742  19.23vv  1809  sbanv  1814  pm11.53  1820  nfsbxy  1863  nfsbxyt  1864  sbcomxyyz  1891  sb9  1900  sbnf2  1902  2sb6  1905  sbcom2v  1906  sb6a  1909  2sb6rf  1911  sbalyz  1920  sbal  1921  sbal1yz  1922  sbal1  1923  sbalv  1926  2exsb  1930  nfsb4t  1935  dvelimf  1936  dveeq1  1940  sbal2  1943  sb8eu  1958  sb8euh  1968  eu1  1970  eu2  1989  mo3h  1998  moanim  2019  2eu4  2038  exists1  2041  eqcom  2087  hblem  2192  abeq2  2193  abeq1  2194  nfceqi  2221  abid2f  2249  dfrex2dc  2367  ralbii2  2384  r2alf  2391  nfraldya  2408  r3al  2416  r19.21t  2444  r19.23t  2475  rabid2  2539  rabbi  2540  ralv  2630  ceqsralt  2640  gencbval  2661  rspc2gv  2725  ralab  2766  ralrab2  2771  euind  2793  reu2  2794  reu3  2796  rmo4  2799  reu8  2802  rmoim  2805  2reuswapdc  2808  reuind  2809  2rmorex  2810  ra5  2916  rmo2ilem  2917  rmo3  2919  dfss2  3003  ss2ab  3078  ss2rab  3086  rabss  3087  uniiunlem  3098  dfdif3  3099  ddifstab  3121  ssequn1  3159  unss  3163  ralunb  3170  ssin  3211  ssddif  3222  n0rf  3284  eq0  3290  eqv  3291  rabeq0  3301  abeq0  3302  disj  3319  disj3  3323  rgenm  3371  pwss  3430  ralsnsg  3463  ralsns  3464  disjsn  3487  euabsn2  3494  snss  3549  snsssn  3588  dfnfc2  3654  uni0b  3661  unissb  3666  elintrab  3683  ssintrab  3694  intun  3702  intpr  3703  dfiin2g  3746  iunss  3754  dfdisj2  3803  cbvdisj  3811  dftr2  3913  dftr5  3914  trint  3926  zfnuleu  3938  vnex  3945  inex1  3948  repizf2lem  3971  axpweq  3981  zfpow  3985  axpow2  3986  axpow3  3987  exmid01  4006  zfpair2  4011  ssextss  4021  frirrg  4151  sucel  4211  zfun  4235  uniex2  4237  setindel  4327  setind  4328  elirr  4330  en2lp  4343  zfregfr  4362  tfi  4370  peano5  4386  ssrel  4494  ssrel2  4496  eqrelrel  4507  reliun  4526  raliunxp  4545  relop  4554  dmopab3  4617  dm0rn0  4621  reldm0  4622  cotr  4780  issref  4781  asymref  4784  intirr  4785  sb8iota  4953  dffun2  4991  dffun4  4992  dffun6f  4994  dffun4f  4997  dffun7  5007  funopab  5014  funcnv2  5039  funcnv  5040  funcnveq  5042  fun2cnv  5043  fun11  5046  fununi  5047  funcnvuni  5048  funimaexglem  5062  fnres  5095  fnopabg  5102  rexrnmpt  5405  dff13  5508  oprabidlem  5637  eqoprab2b  5664  mpt22eqb  5711  ralrnmpt2  5716  dfer2  6245  ltexprlemdisj  7109  recexprlemdisj  7133  isprm2  10981  bj-nfalt  11110  bdceq  11178  bdcriota  11219  bj-axempty2  11230  bj-vprc  11232  bdinex1  11235  bj-zfpair2  11246  bj-uniex2  11252  bj-ssom  11276  bj-inf2vnlem2  11311  ss1oel2o  11333
  Copyright terms: Public domain W3C validator