![]() |
Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > ILE Home > Th. List > gen2 | Unicode 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: ![]() |
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 4266 eusv1 4467 ordtriexmidlem 4533 ordtri2or2exmidlem 4540 onsucelsucexmidlem 4543 ordom 4621 mosubop 4707 eqrelriv 4734 opabid2 4773 xpidtr 5034 funinsn 5281 funoprab 5992 mpofun 5994 fnoprab 5995 elovmpo 6091 mpofvexi 6226 tfrlem7 6337 oaexg 6468 omexg 6471 oeiexg 6473 infiexmid 6900 domfiexmid 6901 climeu 11331 |
Copyright terms: Public domain | W3C validator |