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

Theorem gen2 1547
Description: Generalization applied twice. (Contributed by NM, 30-Apr-1998.)
Hypothesis
Ref Expression
gen2.1 φ
Assertion
Ref Expression
gen2 xyφ

Proof of Theorem gen2
StepHypRef Expression
1 gen2.1 . . 3 φ
21ax-gen 1546 . 2 yφ
32ax-gen 1546 1 xyφ
Colors of variables: wff setvar class
Syntax hints:  wal 1540
This theorem was proved from axioms:  ax-gen 1546
This theorem is referenced by:  euequ1  2292  bm1.1  2338  vtocl3  2911  eueq  3008  csbie2  3181  eqrelkriiv  4213  sikss1c1c  4267  ins2kss  4279  ins3kss  4280  nnsucelr  4428  ssfin  4470  ncfinlower  4483  mosubop  4613  eqoprriv  4853  fvopab4t  5385  1stfo  5505  2ndfo  5506  swapf1o  5511  funoprab  5584  fnoprab  5586  fnfullfunlem2  5857  fvfullfunlem2  5862  fvfullfunlem3  5863  xpassen  6057
  Copyright terms: Public domain W3C validator