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

Theorem 2albii 1641
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 1640 . 2
32albii 1640 1
Colors of variables: wff setvar class
Syntax hints:  <->wb 184  A.wal 1393
This theorem is referenced by:  sbcom2  2189  2sb6rf  2196  mo4f  2336  2mo2  2372  2mos  2375  2eu4OLD  2381  2eu6OLD  2384  r3al  2837  ralcomf  3016  nfnid  4681  raliunxp  5147  cnvsym  5386  intasym  5387  intirr  5390  codir  5392  qfto  5393  dffun4  5605  fun11  5658  fununi  5659  mpt22eqb  6411  aceq0  8520  zfac  8861  zfcndac  9018  addsrmo  9471  mulsrmo  9472  isirred2  17350  2spotdisj  25061  rmo4fOLD  27395  axacprim  29079  dfso2  29183  dfpo2  29184  dfon2lem8  29222  dffun10  29564  wl-sbcom2d  30011  mpt2bi123f  30571  dford4  30971  isdomn3  31164  pm14.12  31328  bnj580  33971  bnj978  34007  cotr2g  37786
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1618  ax-4 1631
This theorem depends on definitions:  df-bi 185
  Copyright terms: Public domain W3C validator