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

Theorem 2albii 1703
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 1702 . 2  |-  ( A. y ph  <->  A. y ps )
32albii 1702 1  |-  ( A. x A. y ph  <->  A. x A. y ps )
Colors of variables: wff setvar class
Syntax hints:    <-> wb 189   A.wal 1453
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1680  ax-4 1693
This theorem depends on definitions:  df-bi 190
This theorem is referenced by:  sbcom2  2285  2sb6rf  2292  mo4f  2356  2mo2  2390  2mos  2392  r3al  2780  ralcomf  2961  nfnid  4643  raliunxp  4993  cnvsym  5233  intasym  5234  intirr  5237  codir  5239  qfto  5240  dffun4  5613  fun11  5670  fununi  5671  mpt22eqb  6432  aceq0  8575  zfac  8916  zfcndac  9070  addsrmo  9523  mulsrmo  9524  cotr2g  13089  isirred2  17978  2spotdisj  25838  rmo4fOLD  28181  bnj580  29773  bnj978  29809  axacprim  30383  dfso2  30443  dfpo2  30444  dfon2lem8  30485  dffun10  30730  wl-sbcom2d  31936  mpt2bi123f  32451  dford4  35929  isdomn3  36126  undmrnresiss  36255  cnvssco  36257  pm14.12  36816
  Copyright terms: Public domain W3C validator