![]() |
Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > ILE Home > Th. List > 2exbidv | GIF version |
Description: Formula-building rule for 2 existential quantifiers (deduction form). (Contributed by NM, 1-May-1995.) |
Ref | Expression |
---|---|
2albidv.1 | ⊢ (𝜑 → (𝜓 ↔ 𝜒)) |
Ref | Expression |
---|---|
2exbidv | ⊢ (𝜑 → (∃𝑥∃𝑦𝜓 ↔ ∃𝑥∃𝑦𝜒)) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | 2albidv.1 | . . 3 ⊢ (𝜑 → (𝜓 ↔ 𝜒)) | |
2 | 1 | exbidv 1825 | . 2 ⊢ (𝜑 → (∃𝑦𝜓 ↔ ∃𝑦𝜒)) |
3 | 2 | exbidv 1825 | 1 ⊢ (𝜑 → (∃𝑥∃𝑦𝜓 ↔ ∃𝑥∃𝑦𝜒)) |
Colors of variables: wff set class |
Syntax hints: → wi 4 ↔ wb 105 ∃wex 1492 |
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 1447 ax-gen 1449 ax-ie1 1493 ax-ie2 1494 ax-4 1510 ax-17 1526 ax-ial 1534 |
This theorem depends on definitions: df-bi 117 |
This theorem is referenced by: 3exbidv 1869 4exbidv 1870 cbvex4v 1930 ceqsex3v 2779 ceqsex4v 2780 copsexg 4244 euotd 4254 elopab 4258 elxpi 4642 relop 4777 cbvoprab3 5950 ov6g 6011 th3qlem1 6636 ltresr 7837 fisumcom2 11445 fprodcom2fi 11633 |
Copyright terms: Public domain | W3C validator |