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

Theorem 2albii 1788
 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 1787 . 2 (∀𝑦𝜑 ↔ ∀𝑦𝜓)
32albii 1787 1 (∀𝑥𝑦𝜑 ↔ ∀𝑥𝑦𝜓)
 Colors of variables: wff setvar class Syntax hints:   ↔ wb 196  ∀wal 1521 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1762  ax-4 1777 This theorem depends on definitions:  df-bi 197 This theorem is referenced by:  sbcom2  2473  2sb6rf  2480  mo4f  2545  2mo2  2579  2mos  2581  r3al  2969  ralcomf  3125  nfnid  4927  raliunxp  5294  cnvsym  5545  intasym  5546  intirr  5549  codir  5551  qfto  5552  dffun4  5938  fun11  6001  fununi  6002  mpt22eqb  6811  aceq0  8979  zfac  9320  zfcndac  9479  addsrmo  9932  mulsrmo  9933  cotr2g  13761  isirred2  18747  rmo4fOLD  29463  bnj580  31109  bnj978  31145  axacprim  31710  dfso2  31770  dfpo2  31771  dfon2lem8  31819  dffun10  32146  wl-sbcom2d  33474  mpt2bi123f  34101  3albii  34154  ssrel3  34208  inxpss  34223  inxpss3  34225  trcoss2  34374  dford4  37913  isdomn3  38099  undmrnresiss  38227  cnvssco  38229  ntrneikb  38709  ntrneixb  38710  pm14.12  38939
 Copyright terms: Public domain W3C validator