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

Theorem gen2 1407
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 1406 . 2  |-  A. y ph
32ax-gen 1406 1  |-  A. x A. y ph
Colors of variables: wff set class
Syntax hints:   A.wal 1310
This theorem was proved from axioms:  ax-gen 1406
This theorem is referenced by:  euequ1  2068  bm1.1  2098  vtocl3  2711  eueq  2822  csbie2  3013  moop2  4131  eusv1  4331  ordtriexmidlem  4393  ordtri2or2exmidlem  4399  onsucelsucexmidlem  4402  ordom  4478  mosubop  4563  eqrelriv  4590  opabid2  4628  xpidtr  4885  funinsn  5128  funoprab  5823  mpofun  5825  fnoprab  5826  elovmpo  5923  mpofvexi  6055  tfrlem7  6165  oaexg  6295  omexg  6298  oeiexg  6300  infiexmid  6721  domfiexmid  6722  climeu  10950
  Copyright terms: Public domain W3C validator