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

Theorem 2albii 1745
Description: Inference adding two universal quantifiers to both sides of an equivalence. (Contributed by NM, 9-Mar-1997.)
Hypothesis
Ref Expression
albii.1 (𝜑𝜓)
Assertion
Ref Expression
2albii (∀𝑥𝑦𝜑 ↔ ∀𝑥𝑦𝜓)

Proof of Theorem 2albii
StepHypRef Expression
1 albii.1 . . 3 (𝜑𝜓)
21albii 1744 . 2 (∀𝑦𝜑 ↔ ∀𝑦𝜓)
32albii 1744 1 (∀𝑥𝑦𝜑 ↔ ∀𝑥𝑦𝜓)
Colors of variables: wff setvar class
Syntax hints:  wb 196  wal 1478
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1719  ax-4 1734
This theorem depends on definitions:  df-bi 197
This theorem is referenced by:  sbcom2  2444  2sb6rf  2451  mo4f  2515  2mo2  2549  2mos  2551  r3al  2935  ralcomf  3088  nfnid  4857  raliunxp  5221  cnvsym  5469  intasym  5470  intirr  5473  codir  5475  qfto  5476  dffun4  5859  fun11  5921  fununi  5922  mpt22eqb  6722  aceq0  8885  zfac  9226  zfcndac  9385  addsrmo  9838  mulsrmo  9839  cotr2g  13649  isirred2  18622  rmo4fOLD  29185  bnj580  30691  bnj978  30727  axacprim  31292  dfso2  31352  dfpo2  31353  dfon2lem8  31396  dffun10  31663  wl-sbcom2d  32976  mpt2bi123f  33603  dford4  37076  isdomn3  37263  undmrnresiss  37391  cnvssco  37393  ntrneikb  37874  ntrneixb  37875  pm14.12  38104
  Copyright terms: Public domain W3C validator