![]() |
Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > ILE Home > Th. List > gen2 | GIF version |
Description: Generalization applied twice. (Contributed by NM, 30-Apr-1998.) |
Ref | Expression |
---|---|
gen2.1 | ⊢ φ |
Ref | Expression |
---|---|
gen2 | ⊢ ∀x∀yφ |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | gen2.1 | . . 3 ⊢ φ | |
2 | 1 | ax-gen 1335 | . 2 ⊢ ∀yφ |
3 | 2 | ax-gen 1335 | 1 ⊢ ∀x∀yφ |
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 |