ILE Home Intuitionistic Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  ILE Home  >  Th. List  >  albii GIF 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 (𝜑𝜓)
Assertion
Ref Expression
albii (∀𝑥𝜑 ↔ ∀𝑥𝜓)

Proof of Theorem albii
StepHypRef Expression
1 albi 1373 . 2 (∀𝑥(𝜑𝜓) → (∀𝑥𝜑 ↔ ∀𝑥𝜓))
2 albii.1 . 2 (𝜑𝜓)
31, 2mpg 1356 1 (∀𝑥𝜑 ↔ ∀𝑥𝜓)
Colors of variables: wff set class
Syntax hints:  wb 102  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  ralab  2723  ralrab2  2728  euind  2750  reu2  2751  reu3  2753  rmo4  2756  reu8  2759  rmoim  2762  2reuswapdc  2765  reuind  2766  2rmorex  2767  ra5  2873  rmo2ilem  2874  rmo3  2876  dfss2  2961  ss2ab  3035  ss2rab  3043  rabss  3044  uniiunlem  3055  ssequn1  3140  unss  3144  ralunb  3151  ssin  3186  ssddif  3198  n0rf  3260  eq0  3266  eqv  3267  rabeq0  3274  abeq0  3275  disj  3295  disj3  3299  rgenm  3350  pwss  3401  ralsnsg  3434  ralsns  3435  disjsn  3459  euabsn2  3466  snss  3521  snsssn  3559  dfnfc2  3625  uni0b  3632  unissb  3637  elintrab  3654  ssintrab  3665  intun  3673  intpr  3674  dfiin2g  3717  iunss  3725  dfdisj2  3774  cbvdisj  3782  dftr2  3883  dftr5  3884  trint  3896  zfnuleu  3908  vprc  3915  inex1  3918  repizf2lem  3941  axpweq  3951  zfpow  3955  axpow2  3956  axpow3  3957  zfpair2  3972  ssextss  3983  frirrg  4114  sucel  4174  zfun  4198  uniex2  4200  setindel  4290  setind  4291  elirr  4293  en2lp  4305  zfregfr  4325  tfi  4332  peano5  4348  ssrel  4455  ssrel2  4457  eqrelrel  4468  reliun  4485  raliunxp  4504  relop  4513  dmopab3  4575  dm0rn0  4579  reldm0  4580  cotr  4733  issref  4734  asymref  4737  intirr  4738  sb8iota  4901  dffun2  4939  dffun4  4940  dffun6f  4942  dffun4f  4945  dffun7  4955  funopab  4962  funcnv2  4986  funcnv  4987  funcnveq  4989  fun2cnv  4990  fun11  4993  fununi  4994  funcnvuni  4995  funimaexglem  5009  fnres  5042  fnopabg  5049  rexrnmpt  5337  dff13  5434  oprabidlem  5563  eqoprab2b  5590  mpt22eqb  5637  ralrnmpt2  5642  dfer2  6137  ltexprlemdisj  6761  recexprlemdisj  6785  bj-nfalt  10277  bdceq  10335  bdcriota  10376  bj-axempty2  10387  bj-vprc  10389  bdinex1  10392  bj-zfpair2  10403  bj-uniex2  10409  bj-ssom  10433  peano5setOLD  10438  bj-inf2vnlem2  10469
  Copyright terms: Public domain W3C validator