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

Theorem 2albii 1820
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 1819 . 2 (∀𝑦𝜑 ↔ ∀𝑦𝜓)
32albii 1819 1 (∀𝑥𝑦𝜑 ↔ ∀𝑥𝑦𝜓)
Colors of variables: wff setvar class
Syntax hints:  wb 206  wal 1538
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809
This theorem depends on definitions:  df-bi 207
This theorem is referenced by:  3albii  1821  sbcom2  2173  2sb6rf  2478  mo4f  2567  2mo2  2647  2mos  2649  2mosOLD  2650  r3al  3197  ralcom  3289  ralcomf  3302  sbccomlem  3869  nfnid  5375  ssrel3  5796  raliunxp  5850  cnvsym  6132  cnvsymOLD  6133  cnvsymOLDOLD  6134  intasym  6135  intirr  6138  codir  6140  qfto  6141  dfpo2  6316  dffun4  6577  fun11  6640  fununi  6641  mpo2eqb  7565  frpoins3xpg  8165  xpord3inddlem  8179  aceq0  10158  zfac  10500  zfcndac  10659  addsrmo  11113  mulsrmo  11114  cotr2g  15015  isirred2  20421  isdomn3  20715  bnj580  34927  bnj978  34963  axacprim  35707  dfso2  35755  dfon2lem8  35791  dffun10  35915  wl-sbcom2d  37562  mpobi123f  38169  r2alan  38250  inxpss  38312  inxpss3  38315  cnvref5  38352  trcoss2  38485  dfantisymrel5  38763  antisymrelres  38764  dford4  43041  undmrnresiss  43617  cnvssco  43619  pm14.12  44440  ichn  47443  dfich2  47445  ichcom  47446  ichbi12i  47447
  Copyright terms: Public domain W3C validator