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

Theorem 2albii 1554
Description: Inference adding 2 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 1553 . 2  |-  ( A. y ph  <->  A. y ps )
32albii 1553 1  |-  ( A. x A. y ph  <->  A. x A. y ps )
Colors of variables: wff set class
Syntax hints:    <-> wb 176   A.wal 1527
This theorem is referenced by:  mo4f  2175  2mos  2222  2eu4  2226  2eu6  2228  ralcomf  2698  nfnid  4204  trsuc2OLD  4477  raliunxp  4825  cnvsym  5057  intasym  5058  intirr  5061  codir  5063  qfto  5064  dffun4  5267  fun11  5315  fununi  5316  mpt22eqb  5953  aceq0  7745  zfac  8086  zfcndac  8241  isirred2  15483  rmo4fOLD  23179  axacprim  24053  dfso2  24111  dfpo2  24112  dfon2lem8  24146  dffun10  24453  isconcl5a  26101  isconcl5ab  26102  dford4  27122  isdomn3  27523  pm14.12  27621  bnj580  28945  bnj978  28981
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1533  ax-5 1544
This theorem depends on definitions:  df-bi 177
  Copyright terms: Public domain W3C validator