Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > ILE Home > Th. List > 4exbidv | Unicode 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 1789 | . 2 |
3 | 2 | 2exbidv 1789 | 1 |
Colors of variables: wff set class |
Syntax hints: wi 4 wb 103 wex 1421 |
This theorem was proved from axioms: ax-1 5 ax-2 6 ax-mp 7 ax-ia1 104 ax-ia2 105 ax-ia3 106 ax-5 1376 ax-gen 1378 ax-ie1 1422 ax-ie2 1423 ax-4 1440 ax-17 1459 ax-ial 1467 |
This theorem depends on definitions: df-bi 115 |
This theorem is referenced by: ceqsex8v 2644 copsex4g 4002 opbrop 4437 ovi3 5657 brecop 6219 th3q 6234 dfplpq2 6544 dfmpq2 6545 enq0sym 6622 enq0ref 6623 enq0tr 6624 enq0breq 6626 addnq0mo 6637 mulnq0mo 6638 addnnnq0 6639 mulnnnq0 6640 addsrmo 6920 mulsrmo 6921 addsrpr 6922 mulsrpr 6923 |
Copyright terms: Public domain | W3C validator |