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

Theorem gen2 1382
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 1381 . 2 𝑦𝜑
32ax-gen 1381 1 𝑥𝑦𝜑
Colors of variables: wff set class
Syntax hints:  wal 1285
This theorem was proved from axioms:  ax-gen 1381
This theorem is referenced by:  euequ1  2040  bm1.1  2070  vtocl3  2669  eueq  2777  csbie2  2966  moop2  4054  eusv1  4250  ordtriexmidlem  4311  ordtri2or2exmidlem  4317  onsucelsucexmidlem  4320  ordom  4396  mosubop  4474  eqrelriv  4501  opabid2  4537  xpidtr  4791  funinsn  5030  funoprab  5704  mpt2fun  5706  fnoprab  5707  elovmpt2  5804  mpt2fvexi  5935  tfrlem7  6038  oaexg  6165  omexg  6168  oeiexg  6170  infiexmid  6547  domfiexmid  6548  climeu  10600
  Copyright terms: Public domain W3C validator