![]() |
Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > ILE Home > Th. List > 2eximi | GIF version |
Description: Inference adding 2 existential quantifiers to antecedent and consequent. (Contributed by NM, 3-Feb-2005.) |
Ref | Expression |
---|---|
eximi.1 | ⊢ (𝜑 → 𝜓) |
Ref | Expression |
---|---|
2eximi | ⊢ (∃𝑥∃𝑦𝜑 → ∃𝑥∃𝑦𝜓) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | eximi.1 | . . 3 ⊢ (𝜑 → 𝜓) | |
2 | 1 | eximi 1536 | . 2 ⊢ (∃𝑦𝜑 → ∃𝑦𝜓) |
3 | 2 | eximi 1536 | 1 ⊢ (∃𝑥∃𝑦𝜑 → ∃𝑥∃𝑦𝜓) |
Colors of variables: wff set class |
Syntax hints: → wi 4 ∃wex 1426 |
This theorem was proved from axioms: ax-1 5 ax-2 6 ax-mp 7 ax-ia1 104 ax-ia2 105 ax-ia3 106 ax-5 1381 ax-gen 1383 ax-ie1 1427 ax-ie2 1428 ax-4 1445 ax-ial 1472 |
This theorem depends on definitions: df-bi 115 |
This theorem is referenced by: excomim 1598 cgsex2g 2655 cgsex4g 2656 vtocl2 2674 vtocl3 2675 dtruarb 4026 opelopabsb 4087 mosubopt 4503 xpmlem 4852 brabvv 5695 ssoprab2i 5737 dmaddpqlem 6934 nqpi 6935 dmaddpq 6936 dmmulpq 6937 enq0sym 6989 enq0ref 6990 enq0tr 6991 nq0nn 6999 prarloc 7060 bj-inex 11753 |
Copyright terms: Public domain | W3C validator |