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 rule). (Contributed by NM, 3-Aug-1995.) |
Ref | Expression |
---|---|
4exbidv.1 | ⊢ (𝜑 → (𝜓 ↔ 𝜒)) |
Ref | Expression |
---|---|
4exbidv | ⊢ (𝜑 → (∃𝑥∃𝑦∃𝑧∃𝑤𝜓 ↔ ∃𝑥∃𝑦∃𝑧∃𝑤𝜒)) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | 4exbidv.1 | . . 3 ⊢ (𝜑 → (𝜓 ↔ 𝜒)) | |
2 | 1 | 2exbidv 1748 | . 2 ⊢ (𝜑 → (∃𝑧∃𝑤𝜓 ↔ ∃𝑧∃𝑤𝜒)) |
3 | 2 | 2exbidv 1748 | 1 ⊢ (𝜑 → (∃𝑥∃𝑦∃𝑧∃𝑤𝜓 ↔ ∃𝑥∃𝑦∃𝑧∃𝑤𝜒)) |
Colors of variables: wff set class |
Syntax hints: → wi 4 ↔ wb 98 ∃wex 1381 |
This theorem was proved from axioms: ax-1 5 ax-2 6 ax-mp 7 ax-ia1 99 ax-ia2 100 ax-ia3 101 ax-5 1336 ax-gen 1338 ax-ie1 1382 ax-ie2 1383 ax-4 1400 ax-17 1419 ax-ial 1427 |
This theorem depends on definitions: df-bi 110 |
This theorem is referenced by: ceqsex8v 2599 copsex4g 3984 opbrop 4419 ovi3 5637 brecop 6196 th3q 6211 dfplpq2 6452 dfmpq2 6453 enq0sym 6530 enq0ref 6531 enq0tr 6532 enq0breq 6534 addnq0mo 6545 mulnq0mo 6546 addnnnq0 6547 mulnnnq0 6548 addsrmo 6828 mulsrmo 6829 addsrpr 6830 mulsrpr 6831 |
Copyright terms: Public domain | W3C validator |