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 1584 | . 2 ⊢ (∃𝑦𝜑 ↔ ∃𝑦𝜓) |
3 | 2 | exbii 1584 | 1 ⊢ (∃𝑥∃𝑦𝜑 ↔ ∃𝑥∃𝑦𝜓) |
Colors of variables: wff set class |
Syntax hints: ↔ wb 104 ∃wex 1468 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-ia1 105 ax-ia2 106 ax-ia3 107 ax-5 1423 ax-gen 1425 ax-ie1 1469 ax-ie2 1470 ax-4 1487 ax-ial 1514 |
This theorem depends on definitions: df-bi 116 |
This theorem is referenced by: 3exbii 1586 19.42vvvv 1885 3exdistr 1887 cbvex4v 1902 ee4anv 1906 ee8anv 1907 sbel2x 1973 2eu4 2092 rexcomf 2593 reean 2599 ceqsex3v 2728 ceqsex4v 2729 ceqsex8v 2731 copsexg 4166 opelopabsbALT 4181 opabm 4202 uniuni 4372 rabxp 4576 elxp3 4593 elvv 4601 elvvv 4602 rexiunxp 4681 elcnv2 4717 cnvuni 4725 coass 5057 fununi 5191 dfmpt3 5245 dfoprab2 5818 dmoprab 5852 rnoprab 5854 mpomptx 5862 resoprab 5867 ovi3 5907 ov6g 5908 oprabex3 6027 xpassen 6724 enq0enq 7239 enq0sym 7240 enq0tr 7242 ltresr 7647 axaddf 7676 axmulf 7677 |
Copyright terms: Public domain | W3C validator |