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

Theorem gen2 1443
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 1442 . 2 𝑦𝜑
32ax-gen 1442 1 𝑥𝑦𝜑
Colors of variables: wff set class
Syntax hints:  wal 1346
This theorem was proved from axioms:  ax-gen 1442
This theorem is referenced by:  euequ1  2114  bm1.1  2155  vtocl3  2786  eueq  2901  csbie2  3098  moop2  4236  eusv1  4437  ordtriexmidlem  4503  ordtri2or2exmidlem  4510  onsucelsucexmidlem  4513  ordom  4591  mosubop  4677  eqrelriv  4704  opabid2  4742  xpidtr  5001  funinsn  5247  funoprab  5953  mpofun  5955  fnoprab  5956  elovmpo  6050  mpofvexi  6185  tfrlem7  6296  oaexg  6427  omexg  6430  oeiexg  6432  infiexmid  6855  domfiexmid  6856  climeu  11259
  Copyright terms: Public domain W3C validator