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

Theorem 2albii 1738
 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 1737 . 2 (∀𝑦𝜑 ↔ ∀𝑦𝜓)
32albii 1737 1 (∀𝑥𝑦𝜑 ↔ ∀𝑥𝑦𝜓)
 Colors of variables: wff setvar class Syntax hints:   ↔ wb 195  ∀wal 1473 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1713  ax-4 1728 This theorem depends on definitions:  df-bi 196 This theorem is referenced by:  sbcom2  2433  2sb6rf  2440  mo4f  2504  2mo2  2538  2mos  2540  r3al  2924  ralcomf  3077  nfnid  4823  raliunxp  5183  cnvsym  5429  intasym  5430  intirr  5433  codir  5435  qfto  5436  dffun4  5816  fun11  5877  fununi  5878  mpt22eqb  6667  aceq0  8824  zfac  9165  zfcndac  9320  addsrmo  9773  mulsrmo  9774  cotr2g  13563  isirred2  18524  2spotdisj  26588  rmo4fOLD  28720  bnj580  30237  bnj978  30273  axacprim  30838  dfso2  30897  dfpo2  30898  dfon2lem8  30939  dffun10  31191  wl-sbcom2d  32523  mpt2bi123f  33141  dford4  36614  isdomn3  36801  undmrnresiss  36929  cnvssco  36931  ntrneikb  37412  ntrneixb  37413  pm14.12  37644
 Copyright terms: Public domain W3C validator