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

Theorem gen2 1430
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 1429 . 2 𝑦𝜑
32ax-gen 1429 1 𝑥𝑦𝜑
Colors of variables: wff set class
Syntax hints:  wal 1333
This theorem was proved from axioms:  ax-gen 1429
This theorem is referenced by:  euequ1  2101  bm1.1  2142  vtocl3  2768  eueq  2883  csbie2  3080  moop2  4213  eusv1  4414  ordtriexmidlem  4480  ordtri2or2exmidlem  4487  onsucelsucexmidlem  4490  ordom  4568  mosubop  4654  eqrelriv  4681  opabid2  4719  xpidtr  4978  funinsn  5221  funoprab  5923  mpofun  5925  fnoprab  5926  elovmpo  6023  mpofvexi  6156  tfrlem7  6266  oaexg  6397  omexg  6400  oeiexg  6402  infiexmid  6824  domfiexmid  6825  climeu  11204
  Copyright terms: Public domain W3C validator