![]() |
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 2782 copsex4g 4247 opbrop 4705 ovi3 6010 brecop 6624 th3q 6639 dfplpq2 7352 dfmpq2 7353 enq0sym 7430 enq0ref 7431 enq0tr 7432 enq0breq 7434 addnq0mo 7445 mulnq0mo 7446 addnnnq0 7447 mulnnnq0 7448 addsrmo 7741 mulsrmo 7742 addsrpr 7743 mulsrpr 7744 |
Copyright terms: Public domain | W3C validator |