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

Theorem gen2 1461
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 1460 . 2  |-  A. y ph
32ax-gen 1460 1  |-  A. x A. y ph
Colors of variables: wff set class
Syntax hints:   A.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  4266  eusv1  4467  ordtriexmidlem  4533  ordtri2or2exmidlem  4540  onsucelsucexmidlem  4543  ordom  4621  mosubop  4707  eqrelriv  4734  opabid2  4773  xpidtr  5034  funinsn  5281  funoprab  5992  mpofun  5994  fnoprab  5995  elovmpo  6091  mpofvexi  6226  tfrlem7  6337  oaexg  6468  omexg  6471  oeiexg  6473  infiexmid  6900  domfiexmid  6901  climeu  11331
  Copyright terms: Public domain W3C validator