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

Theorem gen2 1461
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 1460 . 2 𝑦𝜑
32ax-gen 1460 1 𝑥𝑦𝜑
Colors of variables: wff set class
Syntax hints:  wal 1362
This theorem was proved from axioms:  ax-gen 1460
This theorem is referenced by:  euequ1  2133  bm1.1  2174  vtocl3  2808  eueq  2923  csbie2  3121  moop2  4272  eusv1  4473  ordtriexmidlem  4539  ordtri2or2exmidlem  4546  onsucelsucexmidlem  4549  ordom  4627  mosubop  4713  eqrelriv  4740  opabid2  4779  xpidtr  5040  funinsn  5287  funoprab  6000  mpofun  6002  fnoprab  6003  elovmpo  6099  mpofvexi  6235  tfrlem7  6346  oaexg  6477  omexg  6480  oeiexg  6482  infiexmid  6909  domfiexmid  6910  climeu  11345
  Copyright terms: Public domain W3C validator