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 1410 | . 2 ⊢ ∀𝑦𝜑 |
3 | 2 | ax-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 |