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

Theorem 2albii 1557
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 1556 . 2  |-  ( A. y ph  <->  A. y ps )
32albii 1556 1  |-  ( A. x A. y ph  <->  A. x A. y ps )
Colors of variables: wff set class
Syntax hints:    <-> wb 176   A.wal 1530
This theorem is referenced by:  mo4f  2188  2mos  2235  2eu4  2239  2eu6  2241  ralcomf  2711  nfnid  4220  trsuc2OLD  4493  raliunxp  4841  cnvsym  5073  intasym  5074  intirr  5077  codir  5079  qfto  5080  dffun4  5283  fun11  5331  fununi  5332  mpt22eqb  5969  aceq0  7761  zfac  8102  zfcndac  8257  isirred2  15499  rmo4fOLD  23195  axacprim  24068  dfso2  24182  dfpo2  24183  dfon2lem8  24217  dffun10  24524  isconcl5a  26204  isconcl5ab  26205  dford4  27225  isdomn3  27626  pm14.12  27724  bnj580  29261  bnj978  29297
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1536  ax-5 1547
This theorem depends on definitions:  df-bi 177
  Copyright terms: Public domain W3C validator