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 1429 | . 2 ⊢ ∀𝑦𝜑 |
3 | 2 | ax-gen 1429 | 1 ⊢ ∀𝑥∀𝑦𝜑 |
Colors of variables: wff set class |
Syntax hints: ∀wal 1333 |
This theorem was proved from axioms: ax-gen 1429 |
This theorem is referenced by: euequ1 2101 bm1.1 2142 vtocl3 2768 eueq 2883 csbie2 3080 moop2 4213 eusv1 4414 ordtriexmidlem 4480 ordtri2or2exmidlem 4487 onsucelsucexmidlem 4490 ordom 4568 mosubop 4654 eqrelriv 4681 opabid2 4719 xpidtr 4978 funinsn 5221 funoprab 5923 mpofun 5925 fnoprab 5926 elovmpo 6023 mpofvexi 6156 tfrlem7 6266 oaexg 6397 omexg 6400 oeiexg 6402 infiexmid 6824 domfiexmid 6825 climeu 11204 |
Copyright terms: Public domain | W3C validator |