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 786 | . 2 |
4 | mpjao3dan.3 | . 2 | |
5 | mpjao3dan.4 | . . 3 | |
6 | df-3or 963 | . . 3 | |
7 | 5, 6 | sylib 121 | . 2 |
8 | 3, 4, 7 | mpjaodan 787 | 1 |
Colors of variables: wff set class |
Syntax hints: wi 4 wa 103 wo 697 w3o 961 |
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 698 |
This theorem depends on definitions: df-bi 116 df-3or 963 |
This theorem is referenced by: wetriext 4491 nntri3 6393 nntri2or2 6394 nntr2 6399 tridc 6793 caucvgprlemnkj 7474 caucvgprlemnbj 7475 caucvgprprlemnkj 7500 caucvgprprlemnbj 7501 caucvgsr 7610 npnflt 9598 nmnfgt 9601 xleadd1a 9656 xltadd1 9659 xlt2add 9663 xsubge0 9664 xleaddadd 9670 addmodlteq 10171 iseqf1olemkle 10257 hashfiv01gt1 10528 xrmaxltsup 11027 xrmaxadd 11030 xrbdtri 11045 cvgratz 11301 zdvdsdc 11514 divalglemeunn 11618 divalglemex 11619 divalglemeuneg 11620 divalg 11621 znege1 11856 ennnfonelemk 11913 isxmet2d 12517 nninfalllemn 13202 trilpolemres 13235 |
Copyright terms: Public domain | W3C validator |