Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > ILE Home > Th. List > mpjao3dan | Unicode version |
Description: Eliminate a 3-way disjunction in a deduction. (Contributed by Thierry Arnoux, 13-Apr-2018.) |
Ref | Expression |
---|---|
mpjao3dan.1 | |
mpjao3dan.2 | |
mpjao3dan.3 | |
mpjao3dan.4 |
Ref | Expression |
---|---|
mpjao3dan |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | mpjao3dan.1 | . . 3 | |
2 | mpjao3dan.2 | . . 3 | |
3 | 1, 2 | jaodan 787 | . 2 |
4 | mpjao3dan.3 | . 2 | |
5 | mpjao3dan.4 | . . 3 | |
6 | df-3or 964 | . . 3 | |
7 | 5, 6 | sylib 121 | . 2 |
8 | 3, 4, 7 | mpjaodan 788 | 1 |
Colors of variables: wff set class |
Syntax hints: wi 4 wa 103 wo 698 w3o 962 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-ia1 105 ax-ia2 106 ax-ia3 107 ax-io 699 |
This theorem depends on definitions: df-bi 116 df-3or 964 |
This theorem is referenced by: wetriext 4536 nntri3 6444 nntri2or2 6445 nntr2 6450 tridc 6844 nnnninfeq 7071 exmidontriimlem2 7157 caucvgprlemnkj 7586 caucvgprlemnbj 7587 caucvgprprlemnkj 7612 caucvgprprlemnbj 7613 caucvgsr 7722 npnflt 9719 nmnfgt 9722 xleadd1a 9777 xltadd1 9780 xlt2add 9784 xsubge0 9785 xleaddadd 9791 addmodlteq 10297 iseqf1olemkle 10383 hashfiv01gt1 10656 xrmaxltsup 11155 xrmaxadd 11158 xrbdtri 11173 cvgratz 11429 zdvdsdc 11707 divalglemeunn 11811 divalglemex 11812 divalglemeuneg 11813 divalg 11814 znege1 12052 ennnfonelemk 12129 isxmet2d 12748 trilpolemres 13613 trirec0 13615 |
Copyright terms: Public domain | W3C validator |