![]() |
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 1406 | . 2 ⊢ ∀𝑦𝜑 |
3 | 2 | ax-gen 1406 | 1 ⊢ ∀𝑥∀𝑦𝜑 |
Colors of variables: wff set class |
Syntax hints: ∀wal 1310 |
This theorem was proved from axioms: ax-gen 1406 |
This theorem is referenced by: euequ1 2068 bm1.1 2098 vtocl3 2711 eueq 2822 csbie2 3013 moop2 4131 eusv1 4331 ordtriexmidlem 4393 ordtri2or2exmidlem 4399 onsucelsucexmidlem 4402 ordom 4478 mosubop 4563 eqrelriv 4590 opabid2 4628 xpidtr 4885 funinsn 5128 funoprab 5823 mpofun 5825 fnoprab 5826 elovmpo 5923 mpofvexi 6055 tfrlem7 6165 oaexg 6295 omexg 6298 oeiexg 6300 infiexmid 6721 domfiexmid 6722 climeu 10950 |
Copyright terms: Public domain | W3C validator |