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 1338 | . 2 ⊢ ∀𝑦𝜑 |
3 | 2 | ax-gen 1338 | 1 ⊢ ∀𝑥∀𝑦𝜑 |
Colors of variables: wff set class |
Syntax hints: ∀wal 1241 |
This theorem was proved from axioms: ax-gen 1338 |
This theorem is referenced by: euequ1 1995 bm1.1 2025 vtocl3 2610 eueq 2712 csbie2 2895 moop2 3988 eusv1 4184 ordtriexmidlem 4245 ordtri2or2exmidlem 4251 onsucelsucexmidlem 4254 ordom 4329 mosubop 4406 eqrelriv 4433 opabid2 4467 xpidtr 4715 funoprab 5601 mpt2fun 5603 fnoprab 5604 elovmpt2 5701 mpt2fvexi 5832 tfrlem7 5933 oaexg 6028 omexg 6031 oeiexg 6033 climeu 9817 |
Copyright terms: Public domain | W3C validator |