Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > ILE Home > Th. List > 2exbii | GIF version |
Description: Inference adding 2 existential quantifiers to both sides of an equivalence. (Contributed by NM, 16-Mar-1995.) |
Ref | Expression |
---|---|
exbii.1 | ⊢ (𝜑 ↔ 𝜓) |
Ref | Expression |
---|---|
2exbii | ⊢ (∃𝑥∃𝑦𝜑 ↔ ∃𝑥∃𝑦𝜓) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | exbii.1 | . . 3 ⊢ (𝜑 ↔ 𝜓) | |
2 | 1 | exbii 1496 | . 2 ⊢ (∃𝑦𝜑 ↔ ∃𝑦𝜓) |
3 | 2 | exbii 1496 | 1 ⊢ (∃𝑥∃𝑦𝜑 ↔ ∃𝑥∃𝑦𝜓) |
Colors of variables: wff set class |
Syntax hints: ↔ wb 98 ∃wex 1381 |
This theorem was proved from axioms: ax-1 5 ax-2 6 ax-mp 7 ax-ia1 99 ax-ia2 100 ax-ia3 101 ax-5 1336 ax-gen 1338 ax-ie1 1382 ax-ie2 1383 ax-4 1400 ax-ial 1427 |
This theorem depends on definitions: df-bi 110 |
This theorem is referenced by: 3exbii 1498 19.42vvvv 1790 3exdistr 1792 cbvex4v 1805 ee4anv 1809 ee8anv 1810 sbel2x 1874 2eu4 1993 rexcomf 2472 reean 2478 ceqsex3v 2596 ceqsex4v 2597 ceqsex8v 2599 copsexg 3981 opelopabsbALT 3996 opabm 4017 uniuni 4183 rabxp 4380 elxp3 4394 elvv 4402 elvvv 4403 rexiunxp 4478 elcnv2 4513 cnvuni 4521 coass 4839 fununi 4967 dfmpt3 5021 dfoprab2 5552 dmoprab 5585 rnoprab 5587 mpt2mptx 5595 resoprab 5597 ovi3 5637 ov6g 5638 oprabex3 5756 xpassen 6304 enq0enq 6529 enq0sym 6530 enq0tr 6532 ltresr 6915 |
Copyright terms: Public domain | W3C validator |