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 1442 | . 2 ⊢ ∀𝑦𝜑 |
3 | 2 | ax-gen 1442 | 1 ⊢ ∀𝑥∀𝑦𝜑 |
Colors of variables: wff set class |
Syntax hints: ∀wal 1346 |
This theorem was proved from axioms: ax-gen 1442 |
This theorem is referenced by: euequ1 2114 bm1.1 2155 vtocl3 2786 eueq 2901 csbie2 3098 moop2 4236 eusv1 4437 ordtriexmidlem 4503 ordtri2or2exmidlem 4510 onsucelsucexmidlem 4513 ordom 4591 mosubop 4677 eqrelriv 4704 opabid2 4742 xpidtr 5001 funinsn 5247 funoprab 5953 mpofun 5955 fnoprab 5956 elovmpo 6050 mpofvexi 6185 tfrlem7 6296 oaexg 6427 omexg 6430 oeiexg 6432 infiexmid 6855 domfiexmid 6856 climeu 11259 |
Copyright terms: Public domain | W3C validator |