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

Theorem 2albii 1812
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 1811 . 2 (∀𝑦𝜑 ↔ ∀𝑦𝜓)
32albii 1811 1 (∀𝑥𝑦𝜑 ↔ ∀𝑥𝑦𝜓)
Colors of variables: wff setvar class
Syntax hints:  wb 207  wal 1526
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1787  ax-4 1801
This theorem depends on definitions:  df-bi 208
This theorem is referenced by:  sbcom2  2158  2sb6rf  2489  2sb6rfOLD  2490  mo4f  2644  2mo2  2725  2mos  2727  r3al  3199  ralcom  3351  ralcomf  3354  nfnid  5267  raliunxp  5703  cnvsym  5967  intasym  5968  intirr  5971  codir  5973  qfto  5974  dffun4  6360  fun11  6421  fununi  6422  mpo2eqb  7272  aceq0  9532  zfac  9870  zfcndac  10029  addsrmo  10483  mulsrmo  10484  cotr2g  14324  isirred2  19380  bnj580  32084  bnj978  32120  axacprim  32830  dfso2  32887  dfpo2  32888  dfon2lem8  32932  dffun10  33272  wl-sbcom2d  34678  mpobi123f  35321  3albii  35390  ssrel3  35437  inxpss  35450  inxpss3  35452  trcoss2  35604  dford4  39504  isdomn3  39682  undmrnresiss  39842  cnvssco  39844  pm14.12  40630  dfich2  43490  dfich2ai  43491  ichcom  43494  ichbi12i  43495  ichn  43503
  Copyright terms: Public domain W3C validator