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

Theorem 2albii 1646
Description: Inference adding two universal quantifiers to both sides of an equivalence. (Contributed by NM, 9-Mar-1997.)
Hypothesis
Ref Expression
albii.1  |-  ( ph  <->  ps )
Assertion
Ref Expression
2albii  |-  ( A. x A. y ph  <->  A. x A. y ps )

Proof of Theorem 2albii
StepHypRef Expression
1 albii.1 . . 3  |-  ( ph  <->  ps )
21albii 1645 . 2  |-  ( A. y ph  <->  A. y ps )
32albii 1645 1  |-  ( A. x A. y ph  <->  A. x A. y ps )
Colors of variables: wff setvar class
Syntax hints:    <-> wb 184   A.wal 1396
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1623  ax-4 1636
This theorem depends on definitions:  df-bi 185
This theorem is referenced by:  sbcom2  2191  2sb6rf  2198  mo4f  2334  2mo2  2369  2mos  2372  2eu4OLD  2378  2eu6OLD  2381  r3al  2834  ralcomf  3013  nfnid  4666  raliunxp  5131  cnvsym  5369  intasym  5370  intirr  5373  codir  5375  qfto  5376  dffun4  5582  fun11  5635  fununi  5636  mpt22eqb  6384  aceq0  8490  zfac  8831  zfcndac  8986  addsrmo  9439  mulsrmo  9440  cotr2g  12894  isirred2  17545  2spotdisj  25263  rmo4fOLD  27593  axacprim  29320  dfso2  29424  dfpo2  29425  dfon2lem8  29462  dffun10  29792  wl-sbcom2d  30251  mpt2bi123f  30811  dford4  31210  isdomn3  31405  pm14.12  31569  bnj580  34372  bnj978  34408
  Copyright terms: Public domain W3C validator