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

Theorem 2albii 1896
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 1895 . 2 (∀𝑦𝜑 ↔ ∀𝑦𝜓)
32albii 1895 1 (∀𝑥𝑦𝜑 ↔ ∀𝑥𝑦𝜓)
Colors of variables: wff setvar class
Syntax hints:  wb 196  wal 1629
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1870  ax-4 1885
This theorem depends on definitions:  df-bi 197
This theorem is referenced by:  sbcom2  2593  2sb6rf  2600  mo4f  2665  2mo2  2699  2mos  2701  r3al  3089  ralcomf  3244  nfnid  5025  raliunxp  5400  cnvsym  5651  intasym  5652  intirr  5655  codir  5657  qfto  5658  dffun4  6043  fun11  6103  fununi  6104  mpt22eqb  6916  aceq0  9141  zfac  9484  zfcndac  9643  addsrmo  10096  mulsrmo  10097  cotr2g  13925  isirred2  18909  rmo4fOLD  29675  bnj580  31321  bnj978  31357  axacprim  31922  dfso2  31982  dfpo2  31983  dfon2lem8  32031  dffun10  32358  wl-sbcom2d  33678  mpt2bi123f  34303  3albii  34356  ssrel3  34410  inxpss  34425  inxpss3  34427  trcoss2  34576  dford4  38122  isdomn3  38308  undmrnresiss  38436  cnvssco  38438  ntrneikb  38918  ntrneixb  38919  pm14.12  39148
  Copyright terms: Public domain W3C validator