![]() |
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 1610 | . 2 ⊢ (∃𝑦𝜑 → ∃𝑦𝜓) |
3 | 2 | eximi 1610 | 1 ⊢ (∃𝑥∃𝑦𝜑 → ∃𝑥∃𝑦𝜓) |
Colors of variables: wff set class |
Syntax hints: → wi 4 ∃wex 1502 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-ia1 106 ax-ia2 107 ax-ia3 108 ax-5 1457 ax-gen 1459 ax-ie1 1503 ax-ie2 1504 ax-4 1520 ax-ial 1544 |
This theorem depends on definitions: df-bi 117 |
This theorem is referenced by: excomim 1673 cgsex2g 2785 cgsex4g 2786 vtocl2 2804 vtocl3 2805 dtruarb 4203 opelopabsb 4272 mosubopt 4703 xpmlem 5061 brabvv 5934 ssoprab2i 5977 dmaddpqlem 7390 nqpi 7391 dmaddpq 7392 dmmulpq 7393 enq0sym 7445 enq0ref 7446 enq0tr 7447 nq0nn 7455 prarloc 7516 bj-inex 14955 |
Copyright terms: Public domain | W3C validator |