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

Theorem albii 1431
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 1429 . 2 (∀𝑥(𝜑𝜓) → (∀𝑥𝜑 ↔ ∀𝑥𝜓))
2 albii.1 . 2 (𝜑𝜓)
31, 2mpg 1412 1 (∀𝑥𝜑 ↔ ∀𝑥𝜓)
Colors of variables: wff set class
Syntax hints:  wb 104  wal 1314
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 1408  ax-gen 1410
This theorem depends on definitions:  df-bi 116
This theorem is referenced by:  2albii  1432  hbxfrbi  1433  nfbii  1434  19.26-2  1443  19.26-3an  1444  alrot3  1446  alrot4  1447  albiim  1448  2albiim  1449  alnex  1460  nfalt  1542  aaanh  1550  aaan  1551  alinexa  1567  exintrbi  1597  19.21-2  1630  19.31r  1644  equsalh  1689  equsal  1690  sbcof2  1766  dvelimfALT2  1773  19.23vv  1840  sbanv  1845  pm11.53  1851  nfsbxy  1895  nfsbxyt  1896  sbcomxyyz  1923  sb9  1932  sbnf2  1934  2sb6  1937  sbcom2v  1938  sb6a  1941  2sb6rf  1943  sbalyz  1952  sbal  1953  sbal1yz  1954  sbal1  1955  sbalv  1958  2exsb  1962  nfsb4t  1967  dvelimf  1968  dveeq1  1972  sbal2  1975  sb8eu  1990  sb8euh  2000  eu1  2002  eu2  2021  mo3h  2030  moanim  2051  2eu4  2070  exists1  2073  eqcom  2119  hblem  2225  abeq2  2226  abeq1  2227  nfceqi  2254  abid2f  2283  dfrex2dc  2405  ralbii2  2422  r2alf  2429  nfraldya  2446  r3al  2454  r19.21t  2484  r19.23t  2516  rabid2  2584  rabbi  2585  ralv  2677  ceqsralt  2687  gencbval  2708  rspc2gv  2775  ralab  2817  ralrab2  2822  euind  2844  reu2  2845  reu3  2847  rmo4  2850  reu8  2853  rmo3f  2854  rmoim  2858  2reuswapdc  2861  reuind  2862  2rmorex  2863  ra5  2969  rmo2ilem  2970  rmo3  2972  dfss2  3056  ss2ab  3135  ss2rab  3143  rabss  3144  uniiunlem  3155  dfdif3  3156  ddifstab  3178  ssequn1  3216  unss  3220  ralunb  3227  ssin  3268  ssddif  3280  n0rf  3345  eq0  3351  eqv  3352  rabeq0  3362  abeq0  3363  disj  3381  disj3  3385  rgenm  3435  pwss  3496  ralsnsg  3531  ralsns  3532  disjsn  3555  euabsn2  3562  snss  3619  snsssn  3658  dfnfc2  3724  uni0b  3731  unissb  3736  elintrab  3753  ssintrab  3764  intun  3772  intpr  3773  dfiin2g  3816  iunss  3824  dfdisj2  3878  cbvdisj  3886  disjnim  3890  dftr2  3998  dftr5  3999  trint  4011  zfnuleu  4022  vnex  4029  inex1  4032  repizf2lem  4055  axpweq  4065  zfpow  4069  axpow2  4070  axpow3  4071  exmid01  4091  zfpair2  4102  ssextss  4112  frirrg  4242  sucel  4302  zfun  4326  uniex2  4328  setindel  4423  setind  4424  elirr  4426  en2lp  4439  zfregfr  4458  tfi  4466  peano5  4482  ssrel  4597  ssrel2  4599  eqrelrel  4610  reliun  4630  raliunxp  4650  relop  4659  dmopab3  4722  dm0rn0  4726  reldm0  4727  cotr  4890  issref  4891  asymref  4894  intirr  4895  sb8iota  5065  dffun2  5103  dffun4  5104  dffun6f  5106  dffun4f  5109  dffun7  5120  funopab  5128  funcnv2  5153  funcnv  5154  funcnveq  5156  fun2cnv  5157  fun11  5160  fununi  5161  funcnvuni  5162  funimaexglem  5176  fnres  5209  fnopabg  5216  rexrnmpt  5531  dff13  5637  oprabidlem  5770  eqoprab2b  5797  mpo2eqb  5848  ralrnmpo  5853  dfer2  6398  fiintim  6785  ltexprlemdisj  7382  recexprlemdisj  7406  isprm2  11725  bj-stal  12884  bj-nfalt  12898  bdceq  12967  bdcriota  13008  bj-axempty2  13019  bj-vprc  13021  bdinex1  13024  bj-zfpair2  13035  bj-uniex2  13041  bj-ssom  13061  bj-inf2vnlem2  13096  ss1oel2o  13116
  Copyright terms: Public domain W3C validator