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

Theorem gen2 1411
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 1410 . 2 𝑦𝜑
32ax-gen 1410 1 𝑥𝑦𝜑
Colors of variables: wff set class
Syntax hints:  wal 1314
This theorem was proved from axioms:  ax-gen 1410
This theorem is referenced by:  euequ1  2072  bm1.1  2102  vtocl3  2716  eueq  2828  csbie2  3019  moop2  4143  eusv1  4343  ordtriexmidlem  4405  ordtri2or2exmidlem  4411  onsucelsucexmidlem  4414  ordom  4490  mosubop  4575  eqrelriv  4602  opabid2  4640  xpidtr  4899  funinsn  5142  funoprab  5839  mpofun  5841  fnoprab  5842  elovmpo  5939  mpofvexi  6072  tfrlem7  6182  oaexg  6312  omexg  6315  oeiexg  6317  infiexmid  6739  domfiexmid  6740  climeu  11033
  Copyright terms: Public domain W3C validator