![]() |
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 1868 | . 2 ⊢ (𝜑 → (∃𝑧∃𝑤𝜓 ↔ ∃𝑧∃𝑤𝜒)) |
3 | 2 | 2exbidv 1868 | 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: ceqsex8v 2783 copsex4g 4248 opbrop 4706 ovi3 6011 brecop 6625 th3q 6640 dfplpq2 7353 dfmpq2 7354 enq0sym 7431 enq0ref 7432 enq0tr 7433 enq0breq 7435 addnq0mo 7446 mulnq0mo 7447 addnnnq0 7448 mulnnnq0 7449 addsrmo 7742 mulsrmo 7743 addsrpr 7744 mulsrpr 7745 |
Copyright terms: Public domain | W3C validator |