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

Theorem gen2 1384
Description: Generalization applied twice. (Contributed by NM, 30-Apr-1998.)
Hypothesis
Ref Expression
gen2.1  |-  ph
Assertion
Ref Expression
gen2  |-  A. x A. y ph

Proof of Theorem gen2
StepHypRef Expression
1 gen2.1 . . 3  |-  ph
21ax-gen 1383 . 2  |-  A. y ph
32ax-gen 1383 1  |-  A. x A. y ph
Colors of variables: wff set class
Syntax hints:   A.wal 1287
This theorem was proved from axioms:  ax-gen 1383
This theorem is referenced by:  euequ1  2043  bm1.1  2073  vtocl3  2675  eueq  2784  csbie2  2975  moop2  4069  eusv1  4265  ordtriexmidlem  4326  ordtri2or2exmidlem  4332  onsucelsucexmidlem  4335  ordom  4411  mosubop  4492  eqrelriv  4519  opabid2  4555  xpidtr  4809  funinsn  5049  funoprab  5727  mpt2fun  5729  fnoprab  5730  elovmpt2  5827  mpt2fvexi  5958  tfrlem7  6064  oaexg  6191  omexg  6194  oeiexg  6196  infiexmid  6573  domfiexmid  6574  climeu  10648
  Copyright terms: Public domain W3C validator