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

Theorem 2albii 1915
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 1914 . 2 (∀𝑦𝜑 ↔ ∀𝑦𝜓)
32albii 1914 1 (∀𝑥𝑦𝜑 ↔ ∀𝑥𝑦𝜓)
Colors of variables: wff setvar class
Syntax hints:  wb 197  wal 1650
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1890  ax-4 1904
This theorem depends on definitions:  df-bi 198
This theorem is referenced by:  sbcom2  2536  2sb6rf  2543  mo4f  2636  2mo2  2671  2mos  2673  r3al  3086  ralcomf  3242  nfnid  5010  raliunxp  5429  cnvsym  5692  intasym  5693  intirr  5696  codir  5698  qfto  5699  dffun4  6079  fun11  6140  fununi  6141  mpt22eqb  6966  aceq0  9191  zfac  9534  zfcndac  9693  addsrmo  10146  mulsrmo  10147  cotr2g  14003  isirred2  18967  bnj580  31362  bnj978  31398  axacprim  31961  dfso2  32020  dfpo2  32021  dfon2lem8  32069  dffun10  32396  wl-sbcom2d  33701  mpt2bi123f  34324  3albii  34379  ssrel3  34431  inxpss  34444  inxpss3  34446  trcoss2  34595  eqvrelcoels4  34723  dford4  38205  isdomn3  38391  undmrnresiss  38517  cnvssco  38519  ntrneikb  38998  ntrneixb  38999  pm14.12  39227
  Copyright terms: Public domain W3C validator