![]() |
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 | ⊢ ∀𝑥∀𝑦𝜑 |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | gen2.1 | . . 3 ⊢ 𝜑 | |
2 | 1 | ax-gen 1460 | . 2 ⊢ ∀𝑦𝜑 |
3 | 2 | ax-gen 1460 | 1 ⊢ ∀𝑥∀𝑦𝜑 |
Colors of variables: wff set class |
Syntax hints: ∀wal 1362 |
This theorem was proved from axioms: ax-gen 1460 |
This theorem is referenced by: euequ1 2133 bm1.1 2174 vtocl3 2808 eueq 2923 csbie2 3121 moop2 4272 eusv1 4473 ordtriexmidlem 4539 ordtri2or2exmidlem 4546 onsucelsucexmidlem 4549 ordom 4627 mosubop 4713 eqrelriv 4740 opabid2 4779 xpidtr 5040 funinsn 5287 funoprab 6000 mpofun 6002 fnoprab 6003 elovmpo 6099 mpofvexi 6235 tfrlem7 6346 oaexg 6477 omexg 6480 oeiexg 6482 infiexmid 6909 domfiexmid 6910 climeu 11345 |
Copyright terms: Public domain | W3C validator |