![]() |
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 1803 | . 2 ⊢ (𝜑 → (∃𝑧∃𝑤𝜓 ↔ ∃𝑧∃𝑤𝜒)) |
3 | 2 | 2exbidv 1803 | 1 ⊢ (𝜑 → (∃𝑥∃𝑦∃𝑧∃𝑤𝜓 ↔ ∃𝑥∃𝑦∃𝑧∃𝑤𝜒)) |
Colors of variables: wff set class |
Syntax hints: → wi 4 ↔ wb 104 ∃wex 1433 |
This theorem was proved from axioms: ax-1 5 ax-2 6 ax-mp 7 ax-ia1 105 ax-ia2 106 ax-ia3 107 ax-5 1388 ax-gen 1390 ax-ie1 1434 ax-ie2 1435 ax-4 1452 ax-17 1471 ax-ial 1479 |
This theorem depends on definitions: df-bi 116 |
This theorem is referenced by: ceqsex8v 2678 copsex4g 4098 opbrop 4546 ovi3 5819 brecop 6422 th3q 6437 dfplpq2 7010 dfmpq2 7011 enq0sym 7088 enq0ref 7089 enq0tr 7090 enq0breq 7092 addnq0mo 7103 mulnq0mo 7104 addnnnq0 7105 mulnnnq0 7106 addsrmo 7386 mulsrmo 7387 addsrpr 7388 mulsrpr 7389 |
Copyright terms: Public domain | W3C validator |