Metamath Proof Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >  2albii Structured version   Visualization version   GIF version

Theorem 2albii 1822
 Description: Inference adding two universal quantifiers to both sides of an equivalence. (Contributed by NM, 9-Mar-1997.)
Hypothesis
Ref Expression
albii.1 (𝜑𝜓)
Assertion
Ref Expression
2albii (∀𝑥𝑦𝜑 ↔ ∀𝑥𝑦𝜓)

Proof of Theorem 2albii
StepHypRef Expression
1 albii.1 . . 3 (𝜑𝜓)
21albii 1821 . 2 (∀𝑦𝜑 ↔ ∀𝑦𝜓)
32albii 1821 1 (∀𝑥𝑦𝜑 ↔ ∀𝑥𝑦𝜓)
 Colors of variables: wff setvar class Syntax hints:   ↔ wb 209  ∀wal 1536 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811 This theorem depends on definitions:  df-bi 210 This theorem is referenced by:  sbcom2  2169  2sb6rf  2498  mo4f  2651  2mo2  2732  2mos  2734  r3al  3190  ralcom  3339  ralcomf  3342  nfnid  5249  raliunxp  5683  cnvsym  5947  intasym  5948  intirr  5951  codir  5953  qfto  5954  dffun4  6340  fun11  6401  fununi  6402  mpo2eqb  7257  aceq0  9521  zfac  9859  zfcndac  10018  addsrmo  10472  mulsrmo  10473  cotr2g  14315  isirred2  19429  bnj580  32192  bnj978  32228  axacprim  32940  dfso2  32997  dfpo2  32998  dfon2lem8  33042  dffun10  33382  wl-sbcom2d  34842  mpobi123f  35480  3albii  35549  ssrel3  35596  inxpss  35609  inxpss3  35611  trcoss2  35764  dford4  39767  isdomn3  39945  undmrnresiss  40101  cnvssco  40103  pm14.12  40910  ichn  43766  dfich2  43768  ichcom  43769  ichbi12i  43770
 Copyright terms: Public domain W3C validator