ILE Home Intuitionistic Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  ILE Home  >  Th. List  >  gen2 GIF version

Theorem gen2 1355
Description: Generalization applied twice. (Contributed by NM, 30-Apr-1998.)
Hypothesis
Ref Expression
gen2.1 𝜑
Assertion
Ref Expression
gen2 𝑥𝑦𝜑

Proof of Theorem gen2
StepHypRef Expression
1 gen2.1 . . 3 𝜑
21ax-gen 1354 . 2 𝑦𝜑
32ax-gen 1354 1 𝑥𝑦𝜑
Colors of variables: wff set class
Syntax hints:  wal 1257
This theorem was proved from axioms:  ax-gen 1354
This theorem is referenced by:  euequ1  2011  bm1.1  2041  vtocl3  2627  eueq  2735  csbie2  2923  moop2  4016  eusv1  4212  ordtriexmidlem  4273  ordtri2or2exmidlem  4279  onsucelsucexmidlem  4282  ordom  4357  mosubop  4434  eqrelriv  4461  opabid2  4495  xpidtr  4743  funoprab  5629  mpt2fun  5631  fnoprab  5632  elovmpt2  5729  mpt2fvexi  5860  tfrlem7  5964  oaexg  6059  omexg  6062  oeiexg  6064  climeu  10048
  Copyright terms: Public domain W3C validator