![]() |
Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > ILE Home > Th. List > 4exbidv | GIF version |
Description: Formula-building rule for 4 existential quantifiers (deduction form). (Contributed by NM, 3-Aug-1995.) |
Ref | Expression |
---|---|
4exbidv.1 | ⊢ (𝜑 → (𝜓 ↔ 𝜒)) |
Ref | Expression |
---|---|
4exbidv | ⊢ (𝜑 → (∃𝑥∃𝑦∃𝑧∃𝑤𝜓 ↔ ∃𝑥∃𝑦∃𝑧∃𝑤𝜒)) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | 4exbidv.1 | . . 3 ⊢ (𝜑 → (𝜓 ↔ 𝜒)) | |
2 | 1 | 2exbidv 1878 | . 2 ⊢ (𝜑 → (∃𝑧∃𝑤𝜓 ↔ ∃𝑧∃𝑤𝜒)) |
3 | 2 | 2exbidv 1878 | 1 ⊢ (𝜑 → (∃𝑥∃𝑦∃𝑧∃𝑤𝜓 ↔ ∃𝑥∃𝑦∃𝑧∃𝑤𝜒)) |
Colors of variables: wff set class |
Syntax hints: → wi 4 ↔ wb 105 ∃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-17 1536 ax-ial 1544 |
This theorem depends on definitions: df-bi 117 |
This theorem is referenced by: ceqsex8v 2794 copsex4g 4259 opbrop 4717 ovi3 6025 brecop 6639 th3q 6654 dfplpq2 7367 dfmpq2 7368 enq0sym 7445 enq0ref 7446 enq0tr 7447 enq0breq 7449 addnq0mo 7460 mulnq0mo 7461 addnnnq0 7462 mulnnnq0 7463 addsrmo 7756 mulsrmo 7757 addsrpr 7758 mulsrpr 7759 |
Copyright terms: Public domain | W3C validator |