NFE Home New Foundations Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  NFE Home  >  Th. List  >  2albii GIF version

Theorem 2albii 1567
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 (xyφxyψ)

Proof of Theorem 2albii
StepHypRef Expression
1 albii.1 . . 3 (φψ)
21albii 1566 . 2 (yφyψ)
32albii 1566 1 (xyφxyψ)
Colors of variables: wff setvar class
Syntax hints:  wb 176  wal 1540
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1546  ax-5 1557
This theorem depends on definitions:  df-bi 177
This theorem is referenced by:  mo4f  2236  2mos  2283  2eu4  2287  2eu6  2289  ralcomf  2769  axcnvprim  4091  axssetprim  4092  axsiprim  4093  axins2prim  4095  axins3prim  4096  ssrelk  4211  eqrelk  4212  cnvkexg  4286  ssetkex  4294  sikexlem  4295  sikexg  4296  insklem  4304  ins2kexg  4305  ins3kexg  4306  raliunxp  4823  ssopr  4846  cnvsym  5027  intasym  5028  intirr  5029  dffun2  5119  dffun4  5121  fun11  5159  fununi  5160  enmap2lem4  6066  enmap1lem4  6072
  Copyright terms: Public domain W3C validator