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

Theorem albii 1447
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 1445 . 2 (∀𝑥(𝜑𝜓) → (∀𝑥𝜑 ↔ ∀𝑥𝜓))
2 albii.1 . 2 (𝜑𝜓)
31, 2mpg 1428 1 (∀𝑥𝜑 ↔ ∀𝑥𝜓)
Colors of variables: wff set class
Syntax hints:  wb 104  wal 1330
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 1424  ax-gen 1426
This theorem depends on definitions:  df-bi 116
This theorem is referenced by:  2albii  1448  hbxfrbi  1449  nfbii  1450  19.26-2  1459  19.26-3an  1460  alrot3  1462  alrot4  1463  albiim  1464  2albiim  1465  alnex  1476  nfalt  1558  aaanh  1566  aaan  1567  alinexa  1583  exintrbi  1613  19.21-2  1646  19.31r  1660  equsalh  1705  equsal  1706  sbcof2  1783  dvelimfALT2  1790  19.23vv  1857  sbanv  1862  pm11.53  1868  nfsbxy  1916  nfsbxyt  1917  sbcomxyyz  1946  sb9  1955  sbnf2  1957  2sb6  1960  sbcom2v  1961  sb6a  1964  2sb6rf  1966  sbalyz  1975  sbal  1976  sbal1yz  1977  sbal1  1978  sbalv  1981  2exsb  1985  nfsb4t  1990  dvelimf  1991  dveeq1  1995  sbal2  1998  sb8eu  2013  sb8euh  2023  eu1  2025  eu2  2044  mo3h  2053  moanim  2074  2eu4  2093  exists1  2096  eqcom  2142  hblem  2248  abeq2  2249  abeq1  2250  nfceqi  2278  abid2f  2307  dfrex2dc  2429  ralbii2  2448  r2alf  2455  nfraldya  2472  r3al  2480  r19.21t  2510  r19.23t  2542  rabid2  2610  rabbi  2611  ralv  2706  ceqsralt  2716  gencbval  2737  rspc2gv  2804  ralab  2847  ralrab2  2852  euind  2874  reu2  2875  reu3  2877  rmo4  2880  reu8  2883  rmo3f  2884  rmoim  2888  2reuswapdc  2891  reuind  2892  2rmorex  2893  ra5  3000  rmo2ilem  3001  rmo3  3003  dfss2  3090  ss2ab  3169  ss2rab  3177  rabss  3178  uniiunlem  3189  dfdif3  3190  ddifstab  3212  ssequn1  3250  unss  3254  ralunb  3261  ssin  3302  ssddif  3314  n0rf  3379  eq0  3385  eqv  3386  rabeq0  3396  abeq0  3397  disj  3415  disj3  3419  rgenm  3469  pwss  3530  ralsnsg  3567  ralsns  3568  disjsn  3592  euabsn2  3599  snss  3656  snsssn  3695  dfnfc2  3761  uni0b  3768  unissb  3773  elintrab  3790  ssintrab  3801  intun  3809  intpr  3810  dfiin2g  3853  iunss  3861  dfdisj2  3915  cbvdisj  3923  disjnim  3927  dftr2  4035  dftr5  4036  trint  4048  zfnuleu  4059  vnex  4066  inex1  4069  repizf2lem  4092  axpweq  4102  zfpow  4106  axpow2  4107  axpow3  4108  exmid01  4128  zfpair2  4139  ssextss  4149  frirrg  4279  sucel  4339  zfun  4363  uniex2  4365  setindel  4460  setind  4461  elirr  4463  en2lp  4476  zfregfr  4495  tfi  4503  peano5  4519  ssrel  4634  ssrel2  4636  eqrelrel  4647  reliun  4667  raliunxp  4687  relop  4696  dmopab3  4759  dm0rn0  4763  reldm0  4764  cotr  4927  issref  4928  asymref  4931  intirr  4932  sb8iota  5102  dffun2  5140  dffun4  5141  dffun6f  5143  dffun4f  5146  dffun7  5157  funopab  5165  funcnv2  5190  funcnv  5191  funcnveq  5193  fun2cnv  5194  fun11  5197  fununi  5198  funcnvuni  5199  funimaexglem  5213  fnres  5246  fnopabg  5253  rexrnmpt  5570  dff13  5676  oprabidlem  5809  eqoprab2b  5836  mpo2eqb  5887  ralrnmpo  5892  dfer2  6437  fiintim  6824  omniwomnimkv  7048  ltexprlemdisj  7437  recexprlemdisj  7461  isprm2  11832  bj-stal  13126  bj-nfalt  13140  bdceq  13209  bdcriota  13250  bj-axempty2  13261  bj-vprc  13263  bdinex1  13266  bj-zfpair2  13277  bj-uniex2  13283  bj-ssom  13303  bj-inf2vnlem2  13338  ss1oel2o  13358
  Copyright terms: Public domain W3C validator