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

Theorem gen2 1336
Description: Generalization applied twice. (Contributed by NM, 30-Apr-1998.)
Hypothesis
Ref Expression
gen2.1 φ
Assertion
Ref Expression
gen2 xyφ

Proof of Theorem gen2
StepHypRef Expression
1 gen2.1 . . 3 φ
21ax-gen 1335 . 2 yφ
32ax-gen 1335 1 xyφ
Colors of variables: wff set class
Syntax hints:  wal 1240
This theorem was proved from axioms:  ax-gen 1335
This theorem is referenced by:  euequ1  1992  bm1.1  2022  vtocl3  2604  eueq  2706  csbie2  2889  moop2  3979  eusv1  4150  ordtriexmidlem  4208  onsucelsucexmidlem  4214  ordom  4272  mosubop  4349  eqrelriv  4376  opabid2  4410  xpidtr  4658  funoprab  5543  mpt2fun  5545  fnoprab  5546  elovmpt2  5643  mpt2fvexi  5774  tfrlem7  5874  oaexg  5967  omexg  5970  oeiexg  5972
  Copyright terms: Public domain W3C validator