![]() |
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 | ⊢ (∃x∃yφ ↔ ∃x∃yψ) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | exbii.1 | . . 3 ⊢ (φ ↔ ψ) | |
2 | 1 | exbii 1493 | . 2 ⊢ (∃yφ ↔ ∃yψ) |
3 | 2 | exbii 1493 | 1 ⊢ (∃x∃yφ ↔ ∃x∃yψ) |
Colors of variables: wff set class |
Syntax hints: ↔ wb 98 ∃wex 1378 |
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 1333 ax-gen 1335 ax-ie1 1379 ax-ie2 1380 ax-4 1397 ax-ial 1424 |
This theorem depends on definitions: df-bi 110 |
This theorem is referenced by: 3exbii 1495 19.42vvvv 1787 3exdistr 1789 cbvex4v 1802 ee4anv 1806 ee8anv 1807 sbel2x 1871 2eu4 1990 rexcomf 2466 reean 2472 ceqsex3v 2590 ceqsex4v 2591 ceqsex8v 2593 copsexg 3972 opelopabsbALT 3987 opabm 4008 uniuni 4149 rabxp 4323 elxp3 4337 elvv 4345 elvvv 4346 rexiunxp 4421 elcnv2 4456 cnvuni 4464 coass 4782 fununi 4910 dfmpt3 4964 dfoprab2 5494 dmoprab 5527 rnoprab 5529 mpt2mptx 5537 resoprab 5539 ovi3 5579 ov6g 5580 oprabex3 5698 xpassen 6240 enq0enq 6414 enq0sym 6415 enq0tr 6417 ltresr 6736 |
Copyright terms: Public domain | W3C validator |