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

Theorem gen2 1339
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 1338 . 2 𝑦𝜑
32ax-gen 1338 1 𝑥𝑦𝜑
Colors of variables: wff set class
Syntax hints:  wal 1241
This theorem was proved from axioms:  ax-gen 1338
This theorem is referenced by:  euequ1  1995  bm1.1  2025  vtocl3  2610  eueq  2712  csbie2  2895  moop2  3988  eusv1  4184  ordtriexmidlem  4245  ordtri2or2exmidlem  4251  onsucelsucexmidlem  4254  ordom  4329  mosubop  4406  eqrelriv  4433  opabid2  4467  xpidtr  4715  funoprab  5601  mpt2fun  5603  fnoprab  5604  elovmpt2  5701  mpt2fvexi  5832  tfrlem7  5933  oaexg  6028  omexg  6031  oeiexg  6033  climeu  9817
  Copyright terms: Public domain W3C validator