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

Theorem 2albii 1612
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 1611 . 2  |-  ( A. y ph  <->  A. y ps )
32albii 1611 1  |-  ( A. x A. y ph  <->  A. x A. y ps )
Colors of variables: wff setvar class
Syntax hints:    <-> wb 184   A.wal 1368
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1592  ax-4 1603
This theorem depends on definitions:  df-bi 185
This theorem is referenced by:  sbcom2  2160  2sb6rf  2169  mo4f  2325  2mo2  2368  2mos  2372  2eu4OLD  2378  2eu6OLD  2381  ralcomf  2985  nfnid  4632  raliunxp  5090  cnvsym  5323  intasym  5324  intirr  5327  codir  5329  qfto  5330  dffun4  5541  fun11  5594  fununi  5595  mpt22eqb  6312  aceq0  8403  zfac  8744  zfcndac  8901  isirred2  16926  rmo4fOLD  26059  axacprim  27525  dfso2  27731  dfpo2  27732  dfon2lem8  27770  dffun10  28112  wl-sbcom2d  28558  mpt2bi123f  29146  dford4  29549  isdomn3  29743  pm14.12  29846  2spotdisj  30825  bnj580  32261  bnj978  32297
  Copyright terms: Public domain W3C validator